This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )