Theorem 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	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
	symgfixf.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
	symgfixf.d	⊢ 𝐷 = ( 𝑁 ∖ { 𝐾 } )
Assertion	symgfixelsi	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐹 ∈ 𝑄 ) → ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3		symgfixf.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
4		symgfixf.d	⊢ 𝐷 = ( 𝑁 ∖ { 𝐾 } )
5	1 2	symgfixelq	⊢ ( 𝐹 ∈ 𝑄 → ( 𝐹 ∈ 𝑄 ↔ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) )
6		f1of1	⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 → 𝐹 : 𝑁 –1-1→ 𝑁 )
7	6	ad2antrl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → 𝐹 : 𝑁 –1-1→ 𝑁 )
8		difssd	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 )
9		f1ores	⊢ ( ( 𝐹 : 𝑁 –1-1→ 𝑁 ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) → ( 𝐹 ↾ ( 𝑁 ∖ { 𝐾 } ) ) : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝐹 “ ( 𝑁 ∖ { 𝐾 } ) ) )
10	7 8 9	syl2anc	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝐹 ↾ ( 𝑁 ∖ { 𝐾 } ) ) : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝐹 “ ( 𝑁 ∖ { 𝐾 } ) ) )
11	4	reseq2i	⊢ ( 𝐹 ↾ 𝐷 ) = ( 𝐹 ↾ ( 𝑁 ∖ { 𝐾 } ) )
12	11	a1i	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝐹 ↾ 𝐷 ) = ( 𝐹 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
13	4	a1i	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → 𝐷 = ( 𝑁 ∖ { 𝐾 } ) )
14		f1ofo	⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 → 𝐹 : 𝑁 –onto→ 𝑁 )
15		foima	⊢ ( 𝐹 : 𝑁 –onto→ 𝑁 → ( 𝐹 “ 𝑁 ) = 𝑁 )
16	15	eqcomd	⊢ ( 𝐹 : 𝑁 –onto→ 𝑁 → 𝑁 = ( 𝐹 “ 𝑁 ) )
17	14 16	syl	⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 → 𝑁 = ( 𝐹 “ 𝑁 ) )
18	17	ad2antrl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → 𝑁 = ( 𝐹 “ 𝑁 ) )
19		sneq	⊢ ( 𝐾 = ( 𝐹 ‘ 𝐾 ) → { 𝐾 } = { ( 𝐹 ‘ 𝐾 ) } )
20	19	eqcoms	⊢ ( ( 𝐹 ‘ 𝐾 ) = 𝐾 → { 𝐾 } = { ( 𝐹 ‘ 𝐾 ) } )
21	20	ad2antll	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → { 𝐾 } = { ( 𝐹 ‘ 𝐾 ) } )
22		f1ofn	⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 → 𝐹 Fn 𝑁 )
23	22	ad2antrl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → 𝐹 Fn 𝑁 )
24		simpl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → 𝐾 ∈ 𝑁 )
25		fnsnfv	⊢ ( ( 𝐹 Fn 𝑁 ∧ 𝐾 ∈ 𝑁 ) → { ( 𝐹 ‘ 𝐾 ) } = ( 𝐹 “ { 𝐾 } ) )
26	23 24 25	syl2anc	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → { ( 𝐹 ‘ 𝐾 ) } = ( 𝐹 “ { 𝐾 } ) )
27	21 26	eqtrd	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → { 𝐾 } = ( 𝐹 “ { 𝐾 } ) )
28	18 27	difeq12d	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝑁 ∖ { 𝐾 } ) = ( ( 𝐹 “ 𝑁 ) ∖ ( 𝐹 “ { 𝐾 } ) ) )
29		dff1o2	⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ↔ ( 𝐹 Fn 𝑁 ∧ Fun ◡ 𝐹 ∧ ran 𝐹 = 𝑁 ) )
30	29	simp2bi	⊢ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 → Fun ◡ 𝐹 )
31	30	ad2antrl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → Fun ◡ 𝐹 )
32		imadif	⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( 𝐹 “ 𝑁 ) ∖ ( 𝐹 “ { 𝐾 } ) ) )
33	31 32	syl	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝐹 “ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( 𝐹 “ 𝑁 ) ∖ ( 𝐹 “ { 𝐾 } ) ) )
34	28 13 33	3eqtr4d	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → 𝐷 = ( 𝐹 “ ( 𝑁 ∖ { 𝐾 } ) ) )
35	12 13 34	f1oeq123d	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → ( ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ 𝐷 ↔ ( 𝐹 ↾ ( 𝑁 ∖ { 𝐾 } ) ) : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝐹 “ ( 𝑁 ∖ { 𝐾 } ) ) ) )
36	10 35	mpbird	⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ) → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ 𝐷 )
37	36	ancoms	⊢ ( ( ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ 𝐷 )
38	1 2 3 4	symgfixels	⊢ ( 𝐹 ∈ 𝑄 → ( ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ↔ ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ 𝐷 ) )
39	37 38	imbitrrid	⊢ ( 𝐹 ∈ 𝑄 → ( ( ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) ∧ 𝐾 ∈ 𝑁 ) → ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ) )
40	39	expd	⊢ ( 𝐹 ∈ 𝑄 → ( ( 𝐹 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐹 ‘ 𝐾 ) = 𝐾 ) → ( 𝐾 ∈ 𝑁 → ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ) ) )
41	5 40	sylbid	⊢ ( 𝐹 ∈ 𝑄 → ( 𝐹 ∈ 𝑄 → ( 𝐾 ∈ 𝑁 → ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ) ) )
42	41	pm2.43i	⊢ ( 𝐹 ∈ 𝑄 → ( 𝐾 ∈ 𝑁 → ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 ) )
43	42	impcom	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐹 ∈ 𝑄 ) → ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 )