Theorem symgextf

Description: The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019)

	Ref	Expression
Hypotheses	symgext.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
	symgext.e	⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
Assertion	symgextf	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 ⟶ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		symgext.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2		symgext.e	⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
3		simplll	⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ 𝑥 = 𝐾 ) → 𝐾 ∈ 𝑁 )
4		simpllr	⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → 𝑍 ∈ 𝑆 )
5		simpr	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
6		neqne	⊢ ( ¬ 𝑥 = 𝐾 → 𝑥 ≠ 𝐾 )
7	5 6	anim12i	⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → ( 𝑥 ∈ 𝑁 ∧ 𝑥 ≠ 𝐾 ) )
8		eldifsn	⊢ ( 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ↔ ( 𝑥 ∈ 𝑁 ∧ 𝑥 ≠ 𝐾 ) )
9	7 8	sylibr	⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) )
10		eqid	⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
11	10 1	symgfv	⊢ ( ( 𝑍 ∈ 𝑆 ∧ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑍 ‘ 𝑥 ) ∈ ( 𝑁 ∖ { 𝐾 } ) )
12	4 9 11	syl2anc	⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → ( 𝑍 ‘ 𝑥 ) ∈ ( 𝑁 ∖ { 𝐾 } ) )
13	12	eldifad	⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) ∧ ¬ 𝑥 = 𝐾 ) → ( 𝑍 ‘ 𝑥 ) ∈ 𝑁 )
14	3 13	ifclda	⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑁 ) → if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ∈ 𝑁 )
15	14 2	fmptd	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 ⟶ 𝑁 )