Metamath Proof Explorer

Theorem symgextfv

Description: The function value of the extension of a permutation, fixing the additional element, for elements in the original domain. (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	symgextfv	$⊢ (K \in N \land Z \in S) \to (X \in (N ∖ \{K\}) \to E (X) = Z (X))$

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		eldifi	$⊢ X \in (N ∖ \{K\}) \to X \in N$
4		fvexd	$⊢ (K \in N \land Z \in S) \to Z (X) \in V$
5		ifexg	$⊢ (K \in N \land Z (X) \in V) \to if (X = K, K, Z (X)) \in V$
6	4 5	syldan	$⊢ (K \in N \land Z \in S) \to if (X = K, K, Z (X)) \in V$
7		eqeq1	$⊢ x = X \to (x = K \leftrightarrow X = K)$
8		fveq2	$⊢ x = X \to Z (x) = Z (X)$
9	7 8	ifbieq2d	$⊢ x = X \to if (x = K, K, Z (x)) = if (X = K, K, Z (X))$
10	9 2	fvmptg	$⊢ (X \in N \land if (X = K, K, Z (X)) \in V) \to E (X) = if (X = K, K, Z (X))$
11	3 6 10	syl2anr	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to E (X) = if (X = K, K, Z (X))$
12		eldifsnneq	$⊢ X \in (N ∖ \{K\}) \to \neg X = K$
13	12	adantl	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to \neg X = K$
14	13	iffalsed	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to if (X = K, K, Z (X)) = Z (X)$
15	11 14	eqtrd	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to E (X) = Z (X)$
16	15	ex	$⊢ (K \in N \land Z \in S) \to (X \in (N ∖ \{K\}) \to E (X) = Z (X))$