symgfixelsi

Description: The restriction of a permutation fixing an element to the set with this element removed is an element of the restricted symmetric group. (Contributed by AV, 4-Jan-2019)

	Ref	Expression
Hypotheses	symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
	symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
	symgfixf.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
	symgfixf.d	$⊢ D = N ∖ \{K\}$
Assertion	symgfixelsi	$⊢ (K \in N \land F \in Q) \to {F ↾}_{D} \in S$

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	$⊢ P = {Base}_{SymGrp (N)}$
2		symgfixf.q	$⊢ Q = \{q \in P \| q (K) = K\}$
3		symgfixf.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
4		symgfixf.d	$⊢ D = N ∖ \{K\}$
5	1 2	symgfixelq	$⊢ F \in Q \to (F \in Q \leftrightarrow (F : N \underset{1-1 onto}{⟶} N \land F (K) = K))$
6		f1of1	$⊢ F : N \underset{1-1 onto}{⟶} N \to F : N \underset{1-1}{⟶} N$
7	6	ad2antrl	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to F : N \underset{1-1}{⟶} N$
8		difssd	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to N ∖ \{K\} \subseteq N$
9		f1ores	$⊢ (F : N \underset{1-1}{⟶} N \land N ∖ \{K\} \subseteq N) \to ({F ↾}_{(N ∖ \{K\})}) : N ∖ \{K\} \underset{1-1 onto}{⟶} F [N ∖ \{K\}]$
10	7 8 9	syl2anc	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to ({F ↾}_{(N ∖ \{K\})}) : N ∖ \{K\} \underset{1-1 onto}{⟶} F [N ∖ \{K\}]$
11	4	reseq2i	$⊢ {F ↾}_{D} = {F ↾}_{(N ∖ \{K\})}$
12	11	a1i	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to {F ↾}_{D} = {F ↾}_{(N ∖ \{K\})}$
13	4	a1i	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to D = N ∖ \{K\}$
14		f1ofo	$⊢ F : N \underset{1-1 onto}{⟶} N \to F : N \underset{onto}{⟶} N$
15		foima	$⊢ F : N \underset{onto}{⟶} N \to F [N] = N$
16	15	eqcomd	$⊢ F : N \underset{onto}{⟶} N \to N = F [N]$
17	14 16	syl	$⊢ F : N \underset{1-1 onto}{⟶} N \to N = F [N]$
18	17	ad2antrl	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to N = F [N]$
19		sneq	$⊢ K = F (K) \to \{K\} = \{F (K)\}$
20	19	eqcoms	$⊢ F (K) = K \to \{K\} = \{F (K)\}$
21	20	ad2antll	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to \{K\} = \{F (K)\}$
22		f1ofn	$⊢ F : N \underset{1-1 onto}{⟶} N \to F Fn N$
23	22	ad2antrl	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to F Fn N$
24		simpl	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to K \in N$
25		fnsnfv	$⊢ (F Fn N \land K \in N) \to \{F (K)\} = F [\{K\}]$
26	23 24 25	syl2anc	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to \{F (K)\} = F [\{K\}]$
27	21 26	eqtrd	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to \{K\} = F [\{K\}]$
28	18 27	difeq12d	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to N ∖ \{K\} = F [N] ∖ F [\{K\}]$
29		dff1o2	$⊢ F : N \underset{1-1 onto}{⟶} N \leftrightarrow (F Fn N \land Fun F^{-1} \land ran F = N)$
30	29	simp2bi	$⊢ F : N \underset{1-1 onto}{⟶} N \to Fun F^{-1}$
31	30	ad2antrl	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to Fun F^{-1}$
32		imadif	$⊢ Fun F^{-1} \to F [N ∖ \{K\}] = F [N] ∖ F [\{K\}]$
33	31 32	syl	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to F [N ∖ \{K\}] = F [N] ∖ F [\{K\}]$
34	28 13 33	3eqtr4d	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to D = F [N ∖ \{K\}]$
35	12 13 34	f1oeq123d	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to (({F ↾}_{D}) : D \underset{1-1 onto}{⟶} D \leftrightarrow ({F ↾}_{(N ∖ \{K\})}) : N ∖ \{K\} \underset{1-1 onto}{⟶} F [N ∖ \{K\}])$
36	10 35	mpbird	$⊢ (K \in N \land (F : N \underset{1-1 onto}{⟶} N \land F (K) = K)) \to ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} D$
37	36	ancoms	$⊢ ((F : N \underset{1-1 onto}{⟶} N \land F (K) = K) \land K \in N) \to ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} D$
38	1 2 3 4	symgfixels	$⊢ F \in Q \to ({F ↾}_{D} \in S \leftrightarrow ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} D)$
39	37 38	syl5ibr	$⊢ F \in Q \to (((F : N \underset{1-1 onto}{⟶} N \land F (K) = K) \land K \in N) \to {F ↾}_{D} \in S)$
40	39	expd	$⊢ F \in Q \to ((F : N \underset{1-1 onto}{⟶} N \land F (K) = K) \to (K \in N \to {F ↾}_{D} \in S))$
41	5 40	sylbid	$⊢ F \in Q \to (F \in Q \to (K \in N \to {F ↾}_{D} \in S))$
42	41	pm2.43i	$⊢ F \in Q \to (K \in N \to {F ↾}_{D} \in S)$
43	42	impcom	$⊢ (K \in N \land F \in Q) \to {F ↾}_{D} \in S$

Metamath Proof Explorer

Theorem symgfixelsi

Proof