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={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
	symgext.e	$$⊢E=\left(x\in N⟼if\left(x=K,K,Z\left(x\right)\right)\right)$$
Assertion	symgextfve	$$⊢K\in N\to \left(X=K\to E\left(X\right)=K\right)$$

Proof

Step	Hyp	Ref	Expression
1		symgext.s	$$⊢S={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
2		symgext.e	$$⊢E=\left(x\in N⟼if\left(x=K,K,Z\left(x\right)\right)\right)$$
3		fveq2	$$⊢X=K\to E\left(X\right)=E\left(K\right)$$
4		iftrue	$$⊢x=K\to if\left(x=K,K,Z\left(x\right)\right)=K$$
5	4 2	fvmptg	$$⊢\left(K\in N\wedge K\in N\right)\to E\left(K\right)=K$$
6	5	anidms	$$⊢K\in N\to E\left(K\right)=K$$
7	3 6	sylan9eqr	$$⊢\left(K\in N\wedge X=K\right)\to E\left(X\right)=K$$
8	7	ex	$$⊢K\in N\to \left(X=K\to E\left(X\right)=K\right)$$