Metamath Proof Explorer


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 )