Metamath Proof Explorer

Theorem archiabllem1

Description: Archimedean ordered groups with a minimal positive value are abelian. (Contributed by Thierry Arnoux, 13-Apr-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 )
archiabllem1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
archiabllem1.p ⊢ ( 𝜑 → 0 < 𝑈 )
archiabllem1.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
Assertion archiabllem1 ( 𝜑 → 𝑊 ∈ 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 archiabllem1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
9 archiabllem1.p ⊢ ( 𝜑 → 0 < 𝑈 )
10 archiabllem1.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
11 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
12 6 11 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
13 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑚 ∈ ℤ )
14 13 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑚 ∈ ℂ )
15 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
16 15 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ )
17 14 16 addcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑚 + 𝑛 ) = ( 𝑛 + 𝑚 ) )
18 17 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑚 + 𝑛 ) · 𝑈 ) = ( ( 𝑛 + 𝑚 ) · 𝑈 ) )
19 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑊 ∈ Grp )
20 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑈 ∈ 𝐵 )
21 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
22 1 5 21 mulgdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) ) → ( ( 𝑚 + 𝑛 ) · 𝑈 ) = ( ( 𝑚 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑈 ) ) )
23 19 13 15 20 22 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑚 + 𝑛 ) · 𝑈 ) = ( ( 𝑚 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑈 ) ) )
24 1 5 21 mulgdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) ) → ( ( 𝑛 + 𝑚 ) · 𝑈 ) = ( ( 𝑛 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
25 19 15 13 20 24 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 + 𝑚 ) · 𝑈 ) = ( ( 𝑛 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
26 18 23 25 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑚 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑈 ) ) = ( ( 𝑛 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
27 26 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑚 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑈 ) ) = ( ( 𝑛 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
28 27 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑚 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑈 ) ) = ( ( 𝑛 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
29 28 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑧 = ( 𝑛 · 𝑈 ) ) → ( ( 𝑚 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑈 ) ) = ( ( 𝑛 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
30 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑧 = ( 𝑛 · 𝑈 ) ) → 𝑦 = ( 𝑚 · 𝑈 ) )
31 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑧 = ( 𝑛 · 𝑈 ) ) → 𝑧 = ( 𝑛 · 𝑈 ) )
32 30 31 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑧 = ( 𝑛 · 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( ( 𝑚 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑛 · 𝑈 ) ) )
33 31 30 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑧 = ( 𝑛 · 𝑈 ) ) → ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) = ( ( 𝑛 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
34 29 32 33 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑧 = ( 𝑛 · 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) )
35 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) → 𝜑 )
36 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) ) → 𝑧 ∈ 𝐵 )
37 36 3anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) → 𝑧 ∈ 𝐵 )
38 1 2 3 4 5 6 7 8 9 10 archiabllem1b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑈 ) )
39 35 37 38 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) → ∃ 𝑛 ∈ ℤ 𝑧 = ( 𝑛 · 𝑈 ) )
40 34 39 r19.29a ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑦 = ( 𝑚 · 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) )
41 1 2 3 4 5 6 7 8 9 10 archiabllem1b ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝑚 · 𝑈 ) )
42 41 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝑚 · 𝑈 ) )
43 40 42 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) )
44 43 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) )
45 1 21 isabl2 ⊢ ( 𝑊 ∈ Abel ↔ ( 𝑊 ∈ Grp ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝑊 ) 𝑦 ) ) )
46 12 44 45 sylanbrc ⊢ ( 𝜑 → 𝑊 ∈ Abel )