This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐹 ∈ 𝑄 ) → ( 𝐹 ↾ 𝐷 ) ∈ 𝑆 )