Theorem sgrp2nmndlem5

Description: Lemma 5 for sgrp2nmnd : M is not a monoid. (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Hypotheses	mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
	mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
	sgrp2nmnd.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(x=A,A,B\right)\right)$$
Assertion	sgrp2nmndlem5	$$⊢\left|S\right|=2\to M\notin \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		mgm2nsgrp.s	$$⊢S=\left\{A,B\right\}$$
2		mgm2nsgrp.b	$$⊢{\mathrm{Base}}_M=S$$
3		sgrp2nmnd.o	$$⊢{+}_M=\left(x\in S,y\in S⟼if\left(x=A,A,B\right)\right)$$
4	1	hashprdifel	$$⊢\left|S\right|=2\to \left(A\in S\wedge B\in S\wedge A\ne B\right)$$
5		eqid	$$⊢{+}_M={+}_M$$
6	1 2 3 5	sgrp2nmndlem2	$$⊢\left(A\in S\wedge B\in S\right)\to A{+}_{M}B=A$$
7	6	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A{+}_{M}B=A$$
8		simp3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A\ne B$$
9	7 8	eqnetrd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A{+}_{M}B\ne B$$
10	9	olcd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}A\ne A\vee A{+}_{M}B\ne B\right)$$
11		oveq2	$$⊢y=A\to A{+}_{M}y=A{+}_{M}A$$
12		id	$$⊢y=A\to y=A$$
13	11 12	neeq12d	$$⊢y=A\to \left(A{+}_{M}y\ne y\leftrightarrow A{+}_{M}A\ne A\right)$$
14		oveq2	$$⊢y=B\to A{+}_{M}y=A{+}_{M}B$$
15		id	$$⊢y=B\to y=B$$
16	14 15	neeq12d	$$⊢y=B\to \left(A{+}_{M}y\ne y\leftrightarrow A{+}_{M}B\ne B\right)$$
17	13 16	rexprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\exists y\in \left\{A,B\right\}A{+}_{M}y\ne y\leftrightarrow \left(A{+}_{M}A\ne A\vee A{+}_{M}B\ne B\right)\right)$$
18	17	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\exists y\in \left\{A,B\right\}A{+}_{M}y\ne y\leftrightarrow \left(A{+}_{M}A\ne A\vee A{+}_{M}B\ne B\right)\right)$$
19	10 18	mpbird	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \exists y\in \left\{A,B\right\}A{+}_{M}y\ne y$$
20	1 2 3 5	sgrp2nmndlem3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_{M}A=B$$
21		necom	$$⊢A\ne B\leftrightarrow B\ne A$$
22		df-ne	$$⊢B\ne A\leftrightarrow \neg B=A$$
23	21 22	sylbb	$$⊢A\ne B\to \neg B=A$$
24	23	3ad2ant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \neg B=A$$
25	24	adantr	$$⊢\left(\left(A\in S\wedge B\in S\wedge A\ne B\right)\wedge B{+}_{M}A=B\right)\to \neg B=A$$
26		eqeq1	$$⊢B{+}_{M}A=B\to \left(B{+}_{M}A=A\leftrightarrow B=A\right)$$
27	26	adantl	$$⊢\left(\left(A\in S\wedge B\in S\wedge A\ne B\right)\wedge B{+}_{M}A=B\right)\to \left(B{+}_{M}A=A\leftrightarrow B=A\right)$$
28	25 27	mtbird	$$⊢\left(\left(A\in S\wedge B\in S\wedge A\ne B\right)\wedge B{+}_{M}A=B\right)\to \neg B{+}_{M}A=A$$
29	20 28	mpdan	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \neg B{+}_{M}A=A$$
30	29	neqned	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_{M}A\ne A$$
31	30	orcd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}A\ne A\vee B{+}_{M}B\ne B\right)$$
32		oveq2	$$⊢y=A\to B{+}_{M}y=B{+}_{M}A$$
33	32 12	neeq12d	$$⊢y=A\to \left(B{+}_{M}y\ne y\leftrightarrow B{+}_{M}A\ne A\right)$$
34		oveq2	$$⊢y=B\to B{+}_{M}y=B{+}_{M}B$$
35	34 15	neeq12d	$$⊢y=B\to \left(B{+}_{M}y\ne y\leftrightarrow B{+}_{M}B\ne B\right)$$
36	33 35	rexprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\exists y\in \left\{A,B\right\}B{+}_{M}y\ne y\leftrightarrow \left(B{+}_{M}A\ne A\vee B{+}_{M}B\ne B\right)\right)$$
37	36	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\exists y\in \left\{A,B\right\}B{+}_{M}y\ne y\leftrightarrow \left(B{+}_{M}A\ne A\vee B{+}_{M}B\ne B\right)\right)$$
38	31 37	mpbird	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \exists y\in \left\{A,B\right\}B{+}_{M}y\ne y$$
39		oveq1	$$⊢x=A\to x{+}_{M}y=A{+}_{M}y$$
40	39	neeq1d	$$⊢x=A\to \left(x{+}_{M}y\ne y\leftrightarrow A{+}_{M}y\ne y\right)$$
41	40	rexbidv	$$⊢x=A\to \left(\exists y\in \left\{A,B\right\}x{+}_{M}y\ne y\leftrightarrow \exists y\in \left\{A,B\right\}A{+}_{M}y\ne y\right)$$
42		oveq1	$$⊢x=B\to x{+}_{M}y=B{+}_{M}y$$
43	42	neeq1d	$$⊢x=B\to \left(x{+}_{M}y\ne y\leftrightarrow B{+}_{M}y\ne y\right)$$
44	43	rexbidv	$$⊢x=B\to \left(\exists y\in \left\{A,B\right\}x{+}_{M}y\ne y\leftrightarrow \exists y\in \left\{A,B\right\}B{+}_{M}y\ne y\right)$$
45	41 44	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall x\in \left\{A,B\right\}\exists y\in \left\{A,B\right\}x{+}_{M}y\ne y\leftrightarrow \left(\exists y\in \left\{A,B\right\}A{+}_{M}y\ne y\wedge \exists y\in \left\{A,B\right\}B{+}_{M}y\ne y\right)\right)$$
46	45	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\forall x\in \left\{A,B\right\}\exists y\in \left\{A,B\right\}x{+}_{M}y\ne y\leftrightarrow \left(\exists y\in \left\{A,B\right\}A{+}_{M}y\ne y\wedge \exists y\in \left\{A,B\right\}B{+}_{M}y\ne y\right)\right)$$
47	19 38 46	mpbir2and	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \forall x\in \left\{A,B\right\}\exists y\in \left\{A,B\right\}x{+}_{M}y\ne y$$
48	2 1	eqtr2i	$$⊢\left\{A,B\right\}={\mathrm{Base}}_M$$
49	48 5	isnmnd	$$⊢\forall x\in \left\{A,B\right\}\exists y\in \left\{A,B\right\}x{+}_{M}y\ne y\to M\notin \mathrm{Mnd}$$
50	4 47 49	3syl	$$⊢\left|S\right|=2\to M\notin \mathrm{Mnd}$$