Metamath Proof Explorer


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 ( 𝐾𝑁 → ( 𝑋 = 𝐾 → ( 𝐸𝑋 ) = 𝐾 ) )