Theorem mgm2nsgrplem4

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

	Ref	Expression
Hypotheses	mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
	mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
	mgm2nsgrp.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(\left(x=A\wedge y=A\right),B,A\right)\right)$$
Assertion	mgm2nsgrplem4	Could not format assertion : No typesetting found for |- ( ( # ` S ) = 2 -> M e/ Smgrp ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
2		mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
3		mgm2nsgrp.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(\left(x=A\wedge y=A\right),B,A\right)\right)$$
4	1	hashprdifel	$$⊢\left|S\right|=2\to \left(A\in S\wedge B\in S\wedge A\ne B\right)$$
5		simp1	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A\in S$$
6		simp2	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B\in S$$
7	5 5 6	3jca	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A\in S\wedge A\in S\wedge B\in S\right)$$
8	4 7	syl	$$⊢\left|S\right|=2\to \left(A\in S\wedge A\in S\wedge B\in S\right)$$
9		simp3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A\ne B$$
10		eqid	$$⊢{+}_M={+}_M$$
11	1 2 3 10	mgm2nsgrplem2	$$⊢\left(A\in S\wedge B\in S\right)\to \left(A{+}_{M}A\right){+}_{M}B=A$$
12	11	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}A\right){+}_{M}B=A$$
13	1 2 3 10	mgm2nsgrplem3	$$⊢\left(A\in S\wedge B\in S\right)\to A{+}_M\left(A{+}_{M}B\right)=B$$
14	13	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A{+}_M\left(A{+}_{M}B\right)=B$$
15	9 12 14	3netr4d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}A\right){+}_{M}B\ne A{+}_M\left(A{+}_{M}B\right)$$
16	4 15	syl	$$⊢\left|S\right|=2\to \left(A{+}_{M}A\right){+}_{M}B\ne A{+}_M\left(A{+}_{M}B\right)$$
17	2	eqcomi	$$⊢S={\mathrm{Base}}_M$$
18	17 10	isnsgrp	Could not format ( ( A e. S /\ A e. S /\ B e. S ) -> ( ( ( A ( +g ` M ) A ) ( +g ` M ) B ) =/= ( A ( +g ` M ) ( A ( +g ` M ) B ) ) -> M e/ Smgrp ) ) : No typesetting found for |- ( ( A e. S /\ A e. S /\ B e. S ) -> ( ( ( A ( +g ` M ) A ) ( +g ` M ) B ) =/= ( A ( +g ` M ) ( A ( +g ` M ) B ) ) -> M e/ Smgrp ) ) with typecode |-
19	8 16 18	sylc	Could not format ( ( # ` S ) = 2 -> M e/ Smgrp ) : No typesetting found for |- ( ( # ` S ) = 2 -> M e/ Smgrp ) with typecode |-