Theorem archiabllem2

Description: Archimedean ordered groups with no minimal positive value are abelian. (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)$$
Assertion	archiabllem2	$$⊢\phi \to W\in \mathrm{Abel}$$

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		ogrpgrp	$$⊢W\in \mathrm{oGrp}\to W\in \mathrm{Grp}$$
12	6 11	syl	$$⊢\phi \to W\in \mathrm{Grp}$$
13	6	3ad2ant1	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to W\in \mathrm{oGrp}$$
14	7	3ad2ant1	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to W\in \mathrm{Archi}$$
15	9	3ad2ant1	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to {opp}_{𝑔}\left(W\right)\in \mathrm{oGrp}$$
16		simp1	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to \phi$$
17	16 10	syl3an1	$$⊢\left(\left(\phi \wedge x\in B\wedge y\in B\right)\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)$$
18		simp2	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\in B$$
19		simp3	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to y\in B$$
20	1 2 3 4 5 13 14 8 15 17 18 19	archiabllem2b	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
21	20	3expb	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
22	21	ralrimivva	$$⊢\phi \to \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
23	1 8	isabl2	$$⊢W\in \mathrm{Abel}\leftrightarrow \left(W\in \mathrm{Grp}\wedge \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
24	12 22 23	sylanbrc	$$⊢\phi \to W\in \mathrm{Abel}$$