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→ 𝑆 )