Theorem sgrp2nmndlem4

Description: Lemma 4 for sgrp2nmnd : M is a semigroup. (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	sgrp2nmndlem4	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		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		3simpa	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A\in S\wedge B\in S\right)$$
6	1 2 3	sgrp2nmndlem1	$$⊢\left(A\in S\wedge B\in S\right)\to M\in \mathrm{Mgm}$$
7	4 5 6	3syl	$$⊢\left|S\right|=2\to M\in \mathrm{Mgm}$$
8		eqid	$$⊢{+}_M={+}_M$$
9	1 2 3 8	sgrp2nmndlem2	$$⊢\left(A\in S\wedge A\in S\right)\to A{+}_{M}A=A$$
10	9	oveq1d	$$⊢\left(A\in S\wedge A\in S\right)\to \left(A{+}_{M}A\right){+}_{M}A=A{+}_{M}A$$
11	9	oveq2d	$$⊢\left(A\in S\wedge A\in S\right)\to A{+}_M\left(A{+}_{M}A\right)=A{+}_{M}A$$
12	10 11	eqtr4d	$$⊢\left(A\in S\wedge A\in S\right)\to \left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)$$
13	12	anidms	$$⊢A\in S\to \left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)$$
14	13	3ad2ant1	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)$$
15	9	anidms	$$⊢A\in S\to A{+}_{M}A=A$$
16	15	adantr	$$⊢\left(A\in S\wedge B\in S\right)\to A{+}_{M}A=A$$
17	16	oveq1d	$$⊢\left(A\in S\wedge B\in S\right)\to \left(A{+}_{M}A\right){+}_{M}B=A{+}_{M}B$$
18	1 2 3 8	sgrp2nmndlem2	$$⊢\left(A\in S\wedge B\in S\right)\to A{+}_{M}B=A$$
19	18	oveq2d	$$⊢\left(A\in S\wedge B\in S\right)\to A{+}_M\left(A{+}_{M}B\right)=A{+}_{M}A$$
20	16 19 18	3eqtr4rd	$$⊢\left(A\in S\wedge B\in S\right)\to A{+}_{M}B=A{+}_M\left(A{+}_{M}B\right)$$
21	17 20	eqtrd	$$⊢\left(A\in S\wedge B\in S\right)\to \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)$$
22	21	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)$$
23	14 22	jca	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\wedge \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)$$
24	18	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A{+}_{M}B=A$$
25	1 2 3 8	sgrp2nmndlem3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_{M}A=B$$
26	25	oveq2d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A{+}_M\left(B{+}_{M}A\right)=A{+}_{M}B$$
27	24	oveq1d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}B\right){+}_{M}A=A{+}_{M}A$$
28	15	3ad2ant1	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A{+}_{M}A=A$$
29	27 28	eqtrd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}B\right){+}_{M}A=A$$
30	24 26 29	3eqtr4rd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)$$
31		simp2	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B\in S$$
32	1 2 3 8	sgrp2nmndlem3	$$⊢\left(B\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_{M}B=B$$
33	31 32	syld3an1	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_{M}B=B$$
34	33	oveq2d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to A{+}_M\left(B{+}_{M}B\right)=A{+}_{M}B$$
35	18	oveq1d	$$⊢\left(A\in S\wedge B\in S\right)\to \left(A{+}_{M}B\right){+}_{M}B=A{+}_{M}B$$
36	35 18	eqtrd	$$⊢\left(A\in S\wedge B\in S\right)\to \left(A{+}_{M}B\right){+}_{M}B=A$$
37	36	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}B\right){+}_{M}B=A$$
38	24 34 37	3eqtr4rd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)$$
39	23 30 38	jca32	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\left(\left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\wedge \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)\wedge \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)\right)\right)$$
40	25	oveq1d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}A\right){+}_{M}A=B{+}_{M}A$$
41	28	oveq2d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_M\left(A{+}_{M}A\right)=B{+}_{M}A$$
42	40 41	eqtr4d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)$$
43	24	oveq2d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_M\left(A{+}_{M}B\right)=B{+}_{M}A$$
44	25	oveq1d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}A\right){+}_{M}B=B{+}_{M}B$$
45	44 33	eqtrd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}A\right){+}_{M}B=B$$
46	25 43 45	3eqtr4rd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)$$
47	42 46	jca	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\wedge \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)$$
48	25	oveq2d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_M\left(B{+}_{M}A\right)=B{+}_{M}B$$
49	33	oveq1d	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}B\right){+}_{M}A=B{+}_{M}A$$
50	49 25	eqtrd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}B\right){+}_{M}A=B$$
51	33 48 50	3eqtr4rd	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)$$
52	32	oveq1d	$$⊢\left(B\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}B\right){+}_{M}B=B{+}_{M}B$$
53	32	oveq2d	$$⊢\left(B\in S\wedge B\in S\wedge A\ne B\right)\to B{+}_M\left(B{+}_{M}B\right)=B{+}_{M}B$$
54	52 53	eqtr4d	$$⊢\left(B\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)$$
55	31 54	syld3an1	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)$$
56	47 51 55	jca32	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\left(\left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\wedge \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)\wedge \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)\right)\right)$$
57		oveq1	$$⊢a=A\to a{+}_{M}b=A{+}_{M}b$$
58	57	oveq1d	$$⊢a=A\to \left(a{+}_{M}b\right){+}_{M}c=\left(A{+}_{M}b\right){+}_{M}c$$
59		oveq1	$$⊢a=A\to a{+}_M\left(b{+}_{M}c\right)=A{+}_M\left(b{+}_{M}c\right)$$
60	58 59	eqeq12d	$$⊢a=A\to \left(\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\right)$$
61	60	2ralbidv	$$⊢a=A\to \left(\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\leftrightarrow \forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\right)$$
62		oveq1	$$⊢a=B\to a{+}_{M}b=B{+}_{M}b$$
63	62	oveq1d	$$⊢a=B\to \left(a{+}_{M}b\right){+}_{M}c=\left(B{+}_{M}b\right){+}_{M}c$$
64		oveq1	$$⊢a=B\to a{+}_M\left(b{+}_{M}c\right)=B{+}_M\left(b{+}_{M}c\right)$$
65	63 64	eqeq12d	$$⊢a=B\to \left(\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\right)$$
66	65	2ralbidv	$$⊢a=B\to \left(\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\leftrightarrow \forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\right)$$
67	61 66	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall a\in \left\{A,B\right\}\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\wedge \forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\right)\right)$$
68		oveq2	$$⊢b=A\to A{+}_{M}b=A{+}_{M}A$$
69	68	oveq1d	$$⊢b=A\to \left(A{+}_{M}b\right){+}_{M}c=\left(A{+}_{M}A\right){+}_{M}c$$
70		oveq1	$$⊢b=A\to b{+}_{M}c=A{+}_{M}c$$
71	70	oveq2d	$$⊢b=A\to A{+}_M\left(b{+}_{M}c\right)=A{+}_M\left(A{+}_{M}c\right)$$
72	69 71	eqeq12d	$$⊢b=A\to \left(\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\right)$$
73	72	ralbidv	$$⊢b=A\to \left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\leftrightarrow \forall c\in \left\{A,B\right\}\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\right)$$
74		oveq2	$$⊢b=B\to A{+}_{M}b=A{+}_{M}B$$
75	74	oveq1d	$$⊢b=B\to \left(A{+}_{M}b\right){+}_{M}c=\left(A{+}_{M}B\right){+}_{M}c$$
76		oveq1	$$⊢b=B\to b{+}_{M}c=B{+}_{M}c$$
77	76	oveq2d	$$⊢b=B\to A{+}_M\left(b{+}_{M}c\right)=A{+}_M\left(B{+}_{M}c\right)$$
78	75 77	eqeq12d	$$⊢b=B\to \left(\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\right)$$
79	78	ralbidv	$$⊢b=B\to \left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\leftrightarrow \forall c\in \left\{A,B\right\}\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\right)$$
80	73 79	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\right)\right)$$
81		oveq2	$$⊢b=A\to B{+}_{M}b=B{+}_{M}A$$
82	81	oveq1d	$$⊢b=A\to \left(B{+}_{M}b\right){+}_{M}c=\left(B{+}_{M}A\right){+}_{M}c$$
83	70	oveq2d	$$⊢b=A\to B{+}_M\left(b{+}_{M}c\right)=B{+}_M\left(A{+}_{M}c\right)$$
84	82 83	eqeq12d	$$⊢b=A\to \left(\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\right)$$
85	84	ralbidv	$$⊢b=A\to \left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\leftrightarrow \forall c\in \left\{A,B\right\}\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\right)$$
86		oveq2	$$⊢b=B\to B{+}_{M}b=B{+}_{M}B$$
87	86	oveq1d	$$⊢b=B\to \left(B{+}_{M}b\right){+}_{M}c=\left(B{+}_{M}B\right){+}_{M}c$$
88	76	oveq2d	$$⊢b=B\to B{+}_M\left(b{+}_{M}c\right)=B{+}_M\left(B{+}_{M}c\right)$$
89	87 88	eqeq12d	$$⊢b=B\to \left(\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\right)$$
90	89	ralbidv	$$⊢b=B\to \left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\leftrightarrow \forall c\in \left\{A,B\right\}\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\right)$$
91	85 90	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\right)\right)$$
92	80 91	anbi12d	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\left(\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(A{+}_{M}b\right){+}_{M}c=A{+}_M\left(b{+}_{M}c\right)\wedge \forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(B{+}_{M}b\right){+}_{M}c=B{+}_M\left(b{+}_{M}c\right)\right)\leftrightarrow \left(\left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\right)\wedge \left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\right)\right)\right)$$
93		oveq2	$$⊢c=A\to \left(A{+}_{M}A\right){+}_{M}c=\left(A{+}_{M}A\right){+}_{M}A$$
94		oveq2	$$⊢c=A\to A{+}_{M}c=A{+}_{M}A$$
95	94	oveq2d	$$⊢c=A\to A{+}_M\left(A{+}_{M}c\right)=A{+}_M\left(A{+}_{M}A\right)$$
96	93 95	eqeq12d	$$⊢c=A\to \left(\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\leftrightarrow \left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\right)$$
97		oveq2	$$⊢c=B\to \left(A{+}_{M}A\right){+}_{M}c=\left(A{+}_{M}A\right){+}_{M}B$$
98		oveq2	$$⊢c=B\to A{+}_{M}c=A{+}_{M}B$$
99	98	oveq2d	$$⊢c=B\to A{+}_M\left(A{+}_{M}c\right)=A{+}_M\left(A{+}_{M}B\right)$$
100	97 99	eqeq12d	$$⊢c=B\to \left(\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\leftrightarrow \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)$$
101	96 100	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\leftrightarrow \left(\left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\wedge \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)\right)$$
102		oveq2	$$⊢c=A\to \left(A{+}_{M}B\right){+}_{M}c=\left(A{+}_{M}B\right){+}_{M}A$$
103		oveq2	$$⊢c=A\to B{+}_{M}c=B{+}_{M}A$$
104	103	oveq2d	$$⊢c=A\to A{+}_M\left(B{+}_{M}c\right)=A{+}_M\left(B{+}_{M}A\right)$$
105	102 104	eqeq12d	$$⊢c=A\to \left(\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\leftrightarrow \left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)\right)$$
106		oveq2	$$⊢c=B\to \left(A{+}_{M}B\right){+}_{M}c=\left(A{+}_{M}B\right){+}_{M}B$$
107		oveq2	$$⊢c=B\to B{+}_{M}c=B{+}_{M}B$$
108	107	oveq2d	$$⊢c=B\to A{+}_M\left(B{+}_{M}c\right)=A{+}_M\left(B{+}_{M}B\right)$$
109	106 108	eqeq12d	$$⊢c=B\to \left(\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\leftrightarrow \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)\right)$$
110	105 109	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\leftrightarrow \left(\left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)\wedge \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)\right)\right)$$
111	101 110	anbi12d	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\right)\leftrightarrow \left(\left(\left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\wedge \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)\wedge \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)\right)\right)\right)$$
112		oveq2	$$⊢c=A\to \left(B{+}_{M}A\right){+}_{M}c=\left(B{+}_{M}A\right){+}_{M}A$$
113	94	oveq2d	$$⊢c=A\to B{+}_M\left(A{+}_{M}c\right)=B{+}_M\left(A{+}_{M}A\right)$$
114	112 113	eqeq12d	$$⊢c=A\to \left(\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\leftrightarrow \left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\right)$$
115		oveq2	$$⊢c=B\to \left(B{+}_{M}A\right){+}_{M}c=\left(B{+}_{M}A\right){+}_{M}B$$
116	98	oveq2d	$$⊢c=B\to B{+}_M\left(A{+}_{M}c\right)=B{+}_M\left(A{+}_{M}B\right)$$
117	115 116	eqeq12d	$$⊢c=B\to \left(\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\leftrightarrow \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)$$
118	114 117	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\leftrightarrow \left(\left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\wedge \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)\right)$$
119		oveq2	$$⊢c=A\to \left(B{+}_{M}B\right){+}_{M}c=\left(B{+}_{M}B\right){+}_{M}A$$
120	103	oveq2d	$$⊢c=A\to B{+}_M\left(B{+}_{M}c\right)=B{+}_M\left(B{+}_{M}A\right)$$
121	119 120	eqeq12d	$$⊢c=A\to \left(\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\leftrightarrow \left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)\right)$$
122		oveq2	$$⊢c=B\to \left(B{+}_{M}B\right){+}_{M}c=\left(B{+}_{M}B\right){+}_{M}B$$
123	107	oveq2d	$$⊢c=B\to B{+}_M\left(B{+}_{M}c\right)=B{+}_M\left(B{+}_{M}B\right)$$
124	122 123	eqeq12d	$$⊢c=B\to \left(\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\leftrightarrow \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)\right)$$
125	121 124	ralprg	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\leftrightarrow \left(\left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)\wedge \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)\right)\right)$$
126	118 125	anbi12d	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\right)\leftrightarrow \left(\left(\left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\wedge \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)\wedge \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)\right)\right)\right)$$
127	111 126	anbi12d	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\left(\left(\forall c\in \left\{A,B\right\}\left(A{+}_{M}A\right){+}_{M}c=A{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(A{+}_{M}B\right){+}_{M}c=A{+}_M\left(B{+}_{M}c\right)\right)\wedge \left(\forall c\in \left\{A,B\right\}\left(B{+}_{M}A\right){+}_{M}c=B{+}_M\left(A{+}_{M}c\right)\wedge \forall c\in \left\{A,B\right\}\left(B{+}_{M}B\right){+}_{M}c=B{+}_M\left(B{+}_{M}c\right)\right)\right)\leftrightarrow \left(\left(\left(\left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\wedge \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)\wedge \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)\right)\right)\wedge \left(\left(\left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\wedge \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)\wedge \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)\right)\right)\right)\right)$$
128	67 92 127	3bitrd	$$⊢\left(A\in S\wedge B\in S\right)\to \left(\forall a\in \left\{A,B\right\}\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(\left(\left(\left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\wedge \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)\wedge \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)\right)\right)\wedge \left(\left(\left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\wedge \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)\wedge \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)\right)\right)\right)\right)$$
129	128	3adant3	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \left(\forall a\in \left\{A,B\right\}\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)\leftrightarrow \left(\left(\left(\left(A{+}_{M}A\right){+}_{M}A=A{+}_M\left(A{+}_{M}A\right)\wedge \left(A{+}_{M}A\right){+}_{M}B=A{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(A{+}_{M}B\right){+}_{M}A=A{+}_M\left(B{+}_{M}A\right)\wedge \left(A{+}_{M}B\right){+}_{M}B=A{+}_M\left(B{+}_{M}B\right)\right)\right)\wedge \left(\left(\left(B{+}_{M}A\right){+}_{M}A=B{+}_M\left(A{+}_{M}A\right)\wedge \left(B{+}_{M}A\right){+}_{M}B=B{+}_M\left(A{+}_{M}B\right)\right)\wedge \left(\left(B{+}_{M}B\right){+}_{M}A=B{+}_M\left(B{+}_{M}A\right)\wedge \left(B{+}_{M}B\right){+}_{M}B=B{+}_M\left(B{+}_{M}B\right)\right)\right)\right)\right)$$
130	39 56 129	mpbir2and	$$⊢\left(A\in S\wedge B\in S\wedge A\ne B\right)\to \forall a\in \left\{A,B\right\}\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)$$
131	4 130	syl	$$⊢\left|S\right|=2\to \forall a\in \left\{A,B\right\}\forall b\in \left\{A,B\right\}\forall c\in \left\{A,B\right\}\left(a{+}_{M}b\right){+}_{M}c=a{+}_M\left(b{+}_{M}c\right)$$
132	2 1	eqtr2i	$$⊢\left\{A,B\right\}={\mathrm{Base}}_M$$
133	132 8	issgrp	Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. a e. { A , B } A. b e. { A , B } A. c e. { A , B } ( ( a ( +g ` M ) b ) ( +g ` M ) c ) = ( a ( +g ` M ) ( b ( +g ` M ) c ) ) ) ) with typecode |-
134	7 131 133	sylanbrc	Could not format ( ( # ` S ) = 2 -> M e. Smgrp ) : No typesetting found for |- ( ( # ` S ) = 2 -> M e. Smgrp ) with typecode |-