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 e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion	symgextfve	|- ( K e. N -> ( X = K -> ( E ` X ) = K ) )

Proof

Step	Hyp	Ref	Expression
1		symgext.s	|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
2		symgext.e	|- E = ( x e. 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 e. N /\ K e. N ) -> ( E ` K ) = K )
6	5	anidms	|- ( K e. N -> ( E ` K ) = K )
7	3 6	sylan9eqr	|- ( ( K e. N /\ X = K ) -> ( E ` X ) = K )
8	7	ex	|- ( K e. N -> ( X = K -> ( E ` X ) = K ) )