| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | archiabllem.g | . . 3
⊢ (𝜑 → 𝑊 ∈ oGrp) | 
| 2 |  | ogrpgrp 33081 | . . 3
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝜑 → 𝑊 ∈ Grp) | 
| 4 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑚 ∈ ℤ) | 
| 5 | 4 | zcnd 12725 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑚 ∈ ℂ) | 
| 6 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ) | 
| 7 | 6 | zcnd 12725 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℂ) | 
| 8 | 5, 7 | addcomd 11464 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝑚 + 𝑛) = (𝑛 + 𝑚)) | 
| 9 | 8 | oveq1d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 + 𝑛) · 𝑈) = ((𝑛 + 𝑚) · 𝑈)) | 
| 10 | 3 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑊 ∈ Grp) | 
| 11 |  | archiabllem1.u | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ 𝐵) | 
| 12 | 11 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑈 ∈ 𝐵) | 
| 13 |  | archiabllem.b | . . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑊) | 
| 14 |  | archiabllem.m | . . . . . . . . . . . 12
⊢  · =
(.g‘𝑊) | 
| 15 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(+g‘𝑊) = (+g‘𝑊) | 
| 16 | 13, 14, 15 | mulgdir 19125 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑈 ∈ 𝐵)) → ((𝑚 + 𝑛) · 𝑈) = ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈))) | 
| 17 | 10, 4, 6, 12, 16 | syl13anc 1373 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 + 𝑛) · 𝑈) = ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈))) | 
| 18 | 13, 14, 15 | mulgdir 19125 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵)) → ((𝑛 + 𝑚) · 𝑈) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) | 
| 19 | 10, 6, 4, 12, 18 | syl13anc 1373 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑛 + 𝑚) · 𝑈) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) | 
| 20 | 9, 17, 19 | 3eqtr3d 2784 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) | 
| 21 | 20 | adantllr 719 | . . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) | 
| 22 | 21 | adantlr 715 | . . . . . . 7
⊢
(((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) | 
| 23 | 22 | adantr 480 | . . . . . 6
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) | 
| 24 |  | simpllr 775 | . . . . . . 7
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → 𝑦 = (𝑚 · 𝑈)) | 
| 25 |  | simpr 484 | . . . . . . 7
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → 𝑧 = (𝑛 · 𝑈)) | 
| 26 | 24, 25 | oveq12d 7450 | . . . . . 6
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → (𝑦(+g‘𝑊)𝑧) = ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈))) | 
| 27 | 25, 24 | oveq12d 7450 | . . . . . 6
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → (𝑧(+g‘𝑊)𝑦) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) | 
| 28 | 23, 26, 27 | 3eqtr4d 2786 | . . . . 5
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) | 
| 29 |  | simplll 774 | . . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) → 𝜑) | 
| 30 |  | simpr1r 1231 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℤ ∧ 𝑦 = (𝑚 · 𝑈))) → 𝑧 ∈ 𝐵) | 
| 31 | 30 | 3anassrs 1360 | . . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) → 𝑧 ∈ 𝐵) | 
| 32 |  | archiabllem.0 | . . . . . . 7
⊢  0 =
(0g‘𝑊) | 
| 33 |  | archiabllem.e | . . . . . . 7
⊢  ≤ =
(le‘𝑊) | 
| 34 |  | archiabllem.t | . . . . . . 7
⊢  < =
(lt‘𝑊) | 
| 35 |  | archiabllem.a | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Archi) | 
| 36 |  | archiabllem1.p | . . . . . . 7
⊢ (𝜑 → 0 < 𝑈) | 
| 37 |  | archiabllem1.s | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥) → 𝑈 ≤ 𝑥) | 
| 38 | 13, 32, 33, 34, 14, 1, 35, 11, 36, 37 | archiabllem1b 33200 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑈)) | 
| 39 | 29, 31, 38 | syl2anc 584 | . . . . 5
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) → ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑈)) | 
| 40 | 28, 39 | r19.29a 3161 | . . . 4
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) → (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) | 
| 41 | 13, 32, 33, 34, 14, 1, 35, 11, 36, 37 | archiabllem1b 33200 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑚 ∈ ℤ 𝑦 = (𝑚 · 𝑈)) | 
| 42 | 41 | adantrr 717 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∃𝑚 ∈ ℤ 𝑦 = (𝑚 · 𝑈)) | 
| 43 | 40, 42 | r19.29a 3161 | . . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) | 
| 44 | 43 | ralrimivva 3201 | . 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) | 
| 45 | 13, 15 | isabl2 19809 | . 2
⊢ (𝑊 ∈ Abel ↔ (𝑊 ∈ Grp ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦))) | 
| 46 | 3, 44, 45 | sylanbrc 583 | 1
⊢ (𝜑 → 𝑊 ∈ Abel) |