Theorem archiabllem2b

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 1-May-2018)

	Ref	Expression
Hypotheses	archiabllem.b	$$⊢B={\mathrm{Base}}_W$$
	archiabllem.0	$$⊢\underset{\dot{}}{0}=0_W$$
	archiabllem.e	$$⊢\underset{\dot{}}{\le }={\le }_W$$
	archiabllem.t	$$⊢\underset{\dot{}}{<}={<}_W$$
	archiabllem.m	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	archiabllem.g	$$⊢\phi \to W\in \mathrm{oGrp}$$
	archiabllem.a	$$⊢\phi \to W\in \mathrm{Archi}$$
	archiabllem2.1	$$⊢\underset{\dot{}}{+}={+}_W$$
	archiabllem2.2	$$⊢\phi \to {opp}_{𝑔}\left(W\right)\in \mathrm{oGrp}$$
	archiabllem2.3	$$⊢\left(\phi \wedge a\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}a\right)\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)$$
	archiabllem2b.4	$$⊢\phi \to X\in B$$
	archiabllem2b.5	$$⊢\phi \to Y\in B$$
Assertion	archiabllem2b	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		archiabllem.b	$$⊢B={\mathrm{Base}}_W$$
2		archiabllem.0	$$⊢\underset{\dot{}}{0}=0_W$$
3		archiabllem.e	$$⊢\underset{\dot{}}{\le }={\le }_W$$
4		archiabllem.t	$$⊢\underset{\dot{}}{<}={<}_W$$
5		archiabllem.m	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		archiabllem.g	$$⊢\phi \to W\in \mathrm{oGrp}$$
7		archiabllem.a	$$⊢\phi \to W\in \mathrm{Archi}$$
8		archiabllem2.1	$$⊢\underset{\dot{}}{+}={+}_W$$
9		archiabllem2.2	$$⊢\phi \to {opp}_{𝑔}\left(W\right)\in \mathrm{oGrp}$$
10		archiabllem2.3	$$⊢\left(\phi \wedge a\in B\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}a\right)\to \exists b\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{<}b\wedge b\underset{\dot{}}{<}a\right)$$
11		archiabllem2b.4	$$⊢\phi \to X\in B$$
12		archiabllem2b.5	$$⊢\phi \to Y\in B$$
13	1 2 3 4 5 6 7 8 9 10 11 12	archiabllem2c	$$⊢\phi \to \neg \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{<}\left(Y\underset{\dot{}}{+}X\right)$$
14	1 2 3 4 5 6 7 8 9 10 12 11	archiabllem2c	$$⊢\phi \to \neg \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(X\underset{\dot{}}{+}Y\right)$$
15		isogrp	$$⊢W\in \mathrm{oGrp}\leftrightarrow \left(W\in \mathrm{Grp}\wedge W\in \mathrm{oMnd}\right)$$
16	15	simprbi	$$⊢W\in \mathrm{oGrp}\to W\in \mathrm{oMnd}$$
17		omndtos	$$⊢W\in \mathrm{oMnd}\to W\in \mathrm{Toset}$$
18	6 16 17	3syl	$$⊢\phi \to W\in \mathrm{Toset}$$
19		ogrpgrp	$$⊢W\in \mathrm{oGrp}\to W\in \mathrm{Grp}$$
20	6 19	syl	$$⊢\phi \to W\in \mathrm{Grp}$$
21	1 8	grpcl	$$⊢\left(W\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$
22	20 11 12 21	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$
23	1 8	grpcl	$$⊢\left(W\in \mathrm{Grp}\wedge Y\in B\wedge X\in B\right)\to Y\underset{\dot{}}{+}X\in B$$
24	20 12 11 23	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}X\in B$$
25	1 4	tlt3	$$⊢\left(W\in \mathrm{Toset}\wedge X\underset{\dot{}}{+}Y\in B\wedge Y\underset{\dot{}}{+}X\in B\right)\to \left(X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\vee \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{<}\left(Y\underset{\dot{}}{+}X\right)\vee \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(X\underset{\dot{}}{+}Y\right)\right)$$
26	18 22 24 25	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\vee \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{<}\left(Y\underset{\dot{}}{+}X\right)\vee \left(Y\underset{\dot{}}{+}X\right)\underset{\dot{}}{<}\left(X\underset{\dot{}}{+}Y\right)\right)$$
27	13 14 26	ecase23d	$$⊢\phi \to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$