Theorem symgextfve

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

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

Proof

Step	Hyp	Ref	Expression
1		symgext.s	⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2		symgext.e	⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
3		fveq2	⊢ ( 𝑋 = 𝐾 → ( 𝐸 ‘ 𝑋 ) = ( 𝐸 ‘ 𝐾 ) )
4		iftrue	⊢ ( 𝑥 = 𝐾 → if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) = 𝐾 )
5	4 2	fvmptg	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁 ) → ( 𝐸 ‘ 𝐾 ) = 𝐾 )
6	5	anidms	⊢ ( 𝐾 ∈ 𝑁 → ( 𝐸 ‘ 𝐾 ) = 𝐾 )
7	3 6	sylan9eqr	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑋 = 𝐾 ) → ( 𝐸 ‘ 𝑋 ) = 𝐾 )
8	7	ex	⊢ ( 𝐾 ∈ 𝑁 → ( 𝑋 = 𝐾 → ( 𝐸 ‘ 𝑋 ) = 𝐾 ) )