This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in N ⟼ if (x = K, K, Z (x)))$
Assertion	symgextfve	$⊢ K \in N \to (X = K \to E (X) = K)$

Proof

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