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 S = Base SymGrp N K
symgext.e E = x N if x = K K Z x
Assertion symgextfve K N X = K E X = K

Proof

Step Hyp Ref Expression
1 symgext.s S = Base SymGrp N K
2 symgext.e E = x N if x = K K Z x
3 fveq2 X = K E X = E K
4 iftrue x = K if x = K K Z x = K
5 4 2 fvmptg K N K N E K = K
6 5 anidms K N E K = K
7 3 6 sylan9eqr K N X = K E X = K
8 7 ex K N X = K E X = K