Theorem symgfixf

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

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

Proof

Step	Hyp	Ref	Expression
1		symgfixf.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		symgfixf.q	⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3		symgfixf.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
4		symgfixf.h	⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
5		eqid	⊢ ( 𝑁 ∖ { 𝐾 } ) = ( 𝑁 ∖ { 𝐾 } )
6	1 2 3 5	symgfixelsi	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑞 ∈ 𝑄 ) → ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) ∈ 𝑆 )
7	6 4	fmptd	⊢ ( 𝐾 ∈ 𝑁 → 𝐻 : 𝑄 ⟶ 𝑆 )