mgm2nsgrplem4

Description: Lemma 4 for mgm2nsgrp : M is not a semigroup. (Contributed by AV, 28-Jan-2020) (Proof shortened by AV, 31-Jan-2020)

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	$⊢ S = \{A, B\}$
2		mgm2nsgrp.b	$⊢ {Base}_{M} = S$
3		mgm2nsgrp.o	$⊢ +_{M} = (x \in S, y \in S ⟼ if ((x = A \land y = A), B, A))$
4	1	hashprdifel	$⊢ \|S\| = 2 \to (A \in S \land B \in S \land A \neq B)$
5		simp1	$⊢ (A \in S \land B \in S \land A \neq B) \to A \in S$
6		simp2	$⊢ (A \in S \land B \in S \land A \neq B) \to B \in S$
7	5 5 6	3jca	$⊢ (A \in S \land B \in S \land A \neq B) \to (A \in S \land A \in S \land B \in S)$
8	4 7	syl	$⊢ \|S\| = 2 \to (A \in S \land A \in S \land B \in S)$
9		simp3	$⊢ (A \in S \land B \in S \land A \neq B) \to A \neq B$
10		eqid	$⊢ +_{M} = +_{M}$
11	1 2 3 10	mgm2nsgrplem2	$⊢ (A \in S \land B \in S) \to (A +_{M} A) +_{M} B = A$
12	11	3adant3	$⊢ (A \in S \land B \in S \land A \neq B) \to (A +_{M} A) +_{M} B = A$
13	1 2 3 10	mgm2nsgrplem3	$⊢ (A \in S \land B \in S) \to A +_{M} (A +_{M} B) = B$
14	13	3adant3	$⊢ (A \in S \land B \in S \land A \neq B) \to A +_{M} (A +_{M} B) = B$
15	9 12 14	3netr4d	$⊢ (A \in S \land B \in S \land A \neq B) \to (A +_{M} A) +_{M} B \neq A +_{M} (A +_{M} B)$
16	4 15	syl	$⊢ \|S\| = 2 \to (A +_{M} A) +_{M} B \neq A +_{M} (A +_{M} B)$
17	2	eqcomi	$⊢ S = {Base}_{M}$
18	17 10	isnsgrp	$⊢ (A \in S \land A \in S \land B \in S) \to ((A +_{M} A) +_{M} B \neq A +_{M} (A +_{M} B) \to M \notin Smgrp)$
19	8 16 18	sylc	$⊢ \|S\| = 2 \to M \notin Smgrp$

Metamath Proof Explorer