symgextf1lem

	Ref	Expression
Hypotheses	symgext.s	$⊢ S = {Base}_{SymGrp (N ∖ \{K\})}$
	symgext.e	$⊢ E = (x \in N ⟼ if (x = K, K, Z (x)))$
Assertion	symgextf1lem	$⊢ (K \in N \land Z \in S) \to ((X \in (N ∖ \{K\}) \land Y \in \{K\}) \to E (X) \neq E (Y))$

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		eqid	$⊢ SymGrp (N ∖ \{K\}) = SymGrp (N ∖ \{K\})$
4	3 1	symgfv	$⊢ (Z \in S \land X \in (N ∖ \{K\})) \to Z (X) \in (N ∖ \{K\})$
5	4	adantll	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to Z (X) \in (N ∖ \{K\})$
6		eldifsni	$⊢ Z (X) \in (N ∖ \{K\}) \to Z (X) \neq K$
7	1 2	symgextfv	$⊢ (K \in N \land Z \in S) \to (X \in (N ∖ \{K\}) \to E (X) = Z (X))$
8	7	imp	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to E (X) = Z (X)$
9	8	neeq1d	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to (E (X) \neq K \leftrightarrow Z (X) \neq K)$
10	6 9	syl5ibr	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to (Z (X) \in (N ∖ \{K\}) \to E (X) \neq K)$
11	5 10	mpd	$⊢ ((K \in N \land Z \in S) \land X \in (N ∖ \{K\})) \to E (X) \neq K$
12	11	adantrr	$⊢ ((K \in N \land Z \in S) \land (X \in (N ∖ \{K\}) \land Y \in \{K\})) \to E (X) \neq K$
13		elsni	$⊢ Y \in \{K\} \to Y = K$
14	1 2	symgextfve	$⊢ K \in N \to (Y = K \to E (Y) = K)$
15	14	adantr	$⊢ (K \in N \land Z \in S) \to (Y = K \to E (Y) = K)$
16	13 15	syl5com	$⊢ Y \in \{K\} \to ((K \in N \land Z \in S) \to E (Y) = K)$
17	16	adantl	$⊢ (X \in (N ∖ \{K\}) \land Y \in \{K\}) \to ((K \in N \land Z \in S) \to E (Y) = K)$
18	17	impcom	$⊢ ((K \in N \land Z \in S) \land (X \in (N ∖ \{K\}) \land Y \in \{K\})) \to E (Y) = K$
19	12 18	neeqtrrd	$⊢ ((K \in N \land Z \in S) \land (X \in (N ∖ \{K\}) \land Y \in \{K\})) \to E (X) \neq E (Y)$
20	19	ex	$⊢ (K \in N \land Z \in S) \to ((X \in (N ∖ \{K\}) \land Y \in \{K\}) \to E (X) \neq E (Y))$

Metamath Proof Explorer

Theorem symgextf1lem

Proof