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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	archiabllem.0	⊢ 0 = ( 0g ‘ 𝑊 )
	archiabllem.e	⊢ ≤ = ( le ‘ 𝑊 )
	archiabllem.t	⊢ < = ( lt ‘ 𝑊 )
	archiabllem.m	⊢ · = ( .g ‘ 𝑊 )
	archiabllem.g	⊢ ( 𝜑 → 𝑊 ∈ oGrp )
	archiabllem.a	⊢ ( 𝜑 → 𝑊 ∈ Archi )
	archiabllem2.1	⊢ + = ( +g ‘ 𝑊 )
	archiabllem2.2	⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
	archiabllem2.3	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
Assertion	archiabllem2	⊢ ( 𝜑 → 𝑊 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		archiabllem.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		archiabllem.0	⊢ 0 = ( 0g ‘ 𝑊 )
3		archiabllem.e	⊢ ≤ = ( le ‘ 𝑊 )
4		archiabllem.t	⊢ < = ( lt ‘ 𝑊 )
5		archiabllem.m	⊢ · = ( .g ‘ 𝑊 )
6		archiabllem.g	⊢ ( 𝜑 → 𝑊 ∈ oGrp )
7		archiabllem.a	⊢ ( 𝜑 → 𝑊 ∈ Archi )
8		archiabllem2.1	⊢ + = ( +g ‘ 𝑊 )
9		archiabllem2.2	⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
10		archiabllem2.3	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
11		ogrpgrp	⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
12	6 11	syl	⊢ ( 𝜑 → 𝑊 ∈ Grp )
13	6	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ oGrp )
14	7	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ Archi )
15	9	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( oppg ‘ 𝑊 ) ∈ oGrp )
16		simp1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 )
17	16 10	syl3an1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
18		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
19		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
20	1 2 3 4 5 13 14 8 15 17 18 19	archiabllem2b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
21	20	3expb	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
22	21	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
23	1 8	isabl2	⊢ ( 𝑊 ∈ Abel ↔ ( 𝑊 ∈ Grp ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
24	12 22 23	sylanbrc	⊢ ( 𝜑 → 𝑊 ∈ Abel )