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

Metamath Proof Explorer

Theorem symgfixfo

Description: The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is an onto function. (Contributed by AV, 7-Jan-2019)

Ref Expression
Hypotheses symgfixf.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
symgfixf.q ⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
symgfixf.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
symgfixf.h ⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
Assertion symgfixfo ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –onto→ 𝑆 )

Proof

Step Hyp Ref Expression
1 symgfixf.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 symgfixf.q ⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3 symgfixf.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
4 symgfixf.h ⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
5 1 2 3 4 symgfixf ⊢ ( 𝐾 ∈ 𝑁 → 𝐻 : 𝑄 ⟶ 𝑆 )
6 5 adantl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 ⟶ 𝑆 )
7 eqeq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 = 𝐾 ↔ 𝑗 = 𝐾 ) )
8 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑠 ‘ 𝑖 ) = ( 𝑠 ‘ 𝑗 ) )
9 7 8 ifbieq2d ⊢ ( 𝑖 = 𝑗 → if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) = if ( 𝑗 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑗 ) ) )
10 9 cbvmptv ⊢ ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ if ( 𝑗 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑗 ) ) )
11 1 2 3 4 10 symgfixfolem1 ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ∈ 𝑄 )
12 11 3expa ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ∈ 𝑄 )
13 simpr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐾 ∈ 𝑁 )
14 13 anim1i ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝐾 ∈ 𝑁 ∧ 𝑠 ∈ 𝑆 ) )
15 14 adantl ⊢ ( ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝐾 ∈ 𝑁 ∧ 𝑠 ∈ 𝑆 ) )
16 eqid ⊢ ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) )
17 3 16 symgextres ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑠 )
18 15 17 syl ⊢ ( ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑠 )
19 18 eqcomd ⊢ ( ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) ) → 𝑠 = ( ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
20 reseq1 ⊢ ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) → ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = ( ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
21 20 eqeq2d ⊢ ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) → ( 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ↔ 𝑠 = ( ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
22 21 adantr ⊢ ( ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ↔ 𝑠 = ( ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
23 19 22 mpbird ⊢ ( ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ∧ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) ) → 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
24 23 ex ⊢ ( 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) → ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
25 24 adantl ⊢ ( ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑝 = ( 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , 𝐾 , ( 𝑠 ‘ 𝑖 ) ) ) ) → ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
26 12 25 rspcimedv ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑝 ∈ 𝑄 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
27 26 pm2.43i ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑝 ∈ 𝑄 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
28 4 fvtresfn ⊢ ( 𝑝 ∈ 𝑄 → ( 𝐻 ‘ 𝑝 ) = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
29 28 eqeq2d ⊢ ( 𝑝 ∈ 𝑄 → ( 𝑠 = ( 𝐻 ‘ 𝑝 ) ↔ 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
30 29 adantl ⊢ ( ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑝 ∈ 𝑄 ) → ( 𝑠 = ( 𝐻 ‘ 𝑝 ) ↔ 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
31 30 rexbidva ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → ( ∃ 𝑝 ∈ 𝑄 𝑠 = ( 𝐻 ‘ 𝑝 ) ↔ ∃ 𝑝 ∈ 𝑄 𝑠 = ( 𝑝 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ) )
32 27 31 mpbird ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑝 ∈ 𝑄 𝑠 = ( 𝐻 ‘ 𝑝 ) )
33 32 ralrimiva ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → ∀ 𝑠 ∈ 𝑆 ∃ 𝑝 ∈ 𝑄 𝑠 = ( 𝐻 ‘ 𝑝 ) )
34 dffo3 ⊢ ( 𝐻 : 𝑄 –onto→ 𝑆 ↔ ( 𝐻 : 𝑄 ⟶ 𝑆 ∧ ∀ 𝑠 ∈ 𝑆 ∃ 𝑝 ∈ 𝑄 𝑠 = ( 𝐻 ‘ 𝑝 ) ) )
35 6 33 34 sylanbrc ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ) → 𝐻 : 𝑄 –onto→ 𝑆 )