archiabllem2b

	Ref	Expression
Hypotheses	archiabllem.b	$⊢ B = {Base}_{W}$
	archiabllem.0	$⊢ \underset{˙}{0} = 0_{W}$
	archiabllem.e	$⊢ \underset{˙}{\leq} = \leq_{W}$
	archiabllem.t	$⊢ \underset{˙}{<} = <_{W}$
	archiabllem.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	archiabllem.g	$⊢ φ \to W \in oGrp$
	archiabllem.a	$⊢ φ \to W \in Archi$
	archiabllem2.1	$⊢ \underset{˙}{+} = +_{W}$
	archiabllem2.2	$⊢ φ \to {opp}_{𝑔} (W) \in oGrp$
	archiabllem2.3	$⊢ (φ \land a \in B \land \underset{˙}{0} \underset{˙}{<} a) \to \exists b \in B (\underset{˙}{0} \underset{˙}{<} b \land b \underset{˙}{<} a)$
	archiabllem2b.4	$⊢ φ \to X \in B$
	archiabllem2b.5	$⊢ φ \to Y \in B$
Assertion	archiabllem2b	$⊢ φ \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Proof

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

Metamath Proof Explorer

Theorem archiabllem2b

Proof