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 ⊢ B = Base W
archiabllem.0 ⊢ 0 ˙ = 0 W
archiabllem.e ⊢ ≤ ˙ = ≤ W
archiabllem.t ⊢ < ˙ = < W
archiabllem.m ⊢ · ˙ = ⋅ W
archiabllem.g ⊢ φ → W ∈ oGrp
archiabllem.a ⊢ φ → W ∈ Archi
archiabllem2.1 ⊢ + ˙ = + W
archiabllem2.2 ⊢ φ → opp 𝑔 ⁡ W ∈ oGrp
archiabllem2.3 ⊢ φ ∧ a ∈ B ∧ 0 ˙ < ˙ a → ∃ b ∈ B 0 ˙ < ˙ b ∧ b < ˙ a
Assertion archiabllem2 ⊢ φ → W ∈ Abel

Proof

Step Hyp Ref Expression
1 archiabllem.b ⊢ B = Base W
2 archiabllem.0 ⊢ 0 ˙ = 0 W
3 archiabllem.e ⊢ ≤ ˙ = ≤ W
4 archiabllem.t ⊢ < ˙ = < W
5 archiabllem.m ⊢ · ˙ = ⋅ W
6 archiabllem.g ⊢ φ → W ∈ oGrp
7 archiabllem.a ⊢ φ → W ∈ Archi
8 archiabllem2.1 ⊢ + ˙ = + W
9 archiabllem2.2 ⊢ φ → opp 𝑔 ⁡ W ∈ oGrp
10 archiabllem2.3 ⊢ φ ∧ a ∈ B ∧ 0 ˙ < ˙ a → ∃ b ∈ B 0 ˙ < ˙ b ∧ b < ˙ a
11 ogrpgrp ⊢ W ∈ oGrp → W ∈ Grp
12 6 11 syl ⊢ φ → W ∈ Grp
13 6 3ad2ant1 ⊢ φ ∧ x ∈ B ∧ y ∈ B → W ∈ oGrp
14 7 3ad2ant1 ⊢ φ ∧ x ∈ B ∧ y ∈ B → W ∈ Archi
15 9 3ad2ant1 ⊢ φ ∧ x ∈ B ∧ y ∈ B → opp 𝑔 ⁡ W ∈ oGrp
16 simp1 ⊢ φ ∧ x ∈ B ∧ y ∈ B → φ
17 16 10 syl3an1 ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ a ∈ B ∧ 0 ˙ < ˙ a → ∃ b ∈ B 0 ˙ < ˙ b ∧ b < ˙ a
18 simp2 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ∈ B
19 simp3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ∈ B
20 1 2 3 4 5 13 14 8 15 17 18 19 archiabllem2b ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + ˙ y = y + ˙ x
21 20 3expb ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + ˙ y = y + ˙ x
22 21 ralrimivva ⊢ φ → ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x
23 1 8 isabl2 ⊢ W ∈ Abel ↔ W ∈ Grp ∧ ∀ x ∈ B ∀ y ∈ B x + ˙ y = y + ˙ x
24 12 22 23 sylanbrc ⊢ φ → W ∈ Abel