Step | Hyp | Ref
| Expression |
1 | | archiabllem.g |
. . 3
⊢ (𝜑 → 𝑊 ∈ oGrp) |
2 | | ogrpgrp 29034 |
. . 3
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑊 ∈ Grp) |
4 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑚 ∈ ℤ) |
5 | 4 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑚 ∈ ℂ) |
6 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ) |
7 | 6 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℂ) |
8 | 5, 7 | addcomd 10117 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝑚 + 𝑛) = (𝑛 + 𝑚)) |
9 | 8 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 + 𝑛) · 𝑈) = ((𝑛 + 𝑚) · 𝑈)) |
10 | 3 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑊 ∈ Grp) |
11 | | archiabllem1.u |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ 𝐵) |
12 | 11 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑈 ∈ 𝐵) |
13 | | archiabllem.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑊) |
14 | | archiabllem.m |
. . . . . . . . . . . 12
⊢ · =
(.g‘𝑊) |
15 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝑊) = (+g‘𝑊) |
16 | 13, 14, 15 | mulgdir 17396 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑈 ∈ 𝐵)) → ((𝑚 + 𝑛) · 𝑈) = ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈))) |
17 | 10, 4, 6, 12, 16 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 + 𝑛) · 𝑈) = ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈))) |
18 | 13, 14, 15 | mulgdir 17396 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ (𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵)) → ((𝑛 + 𝑚) · 𝑈) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
19 | 10, 6, 4, 12, 18 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑛 + 𝑚) · 𝑈) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
20 | 9, 17, 19 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
21 | 20 | adantllr 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
22 | 21 | adantlr 747 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
23 | 22 | adantr 480 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈)) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
24 | | simpllr 795 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → 𝑦 = (𝑚 · 𝑈)) |
25 | | simpr 476 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → 𝑧 = (𝑛 · 𝑈)) |
26 | 24, 25 | oveq12d 6567 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → (𝑦(+g‘𝑊)𝑧) = ((𝑚 · 𝑈)(+g‘𝑊)(𝑛 · 𝑈))) |
27 | 25, 24 | oveq12d 6567 |
. . . . . 6
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → (𝑧(+g‘𝑊)𝑦) = ((𝑛 · 𝑈)(+g‘𝑊)(𝑚 · 𝑈))) |
28 | 23, 26, 27 | 3eqtr4d 2654 |
. . . . 5
⊢
((((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) ∧ 𝑛 ∈ ℤ) ∧ 𝑧 = (𝑛 · 𝑈)) → (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) |
29 | | simplll 794 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) → 𝜑) |
30 | | simpr1r 1112 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℤ ∧ 𝑦 = (𝑚 · 𝑈))) → 𝑧 ∈ 𝐵) |
31 | 30 | 3anassrs 1282 |
. . . . . 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 29077 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑈)) |
39 | 29, 31, 38 | syl2anc 691 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) → ∃𝑛 ∈ ℤ 𝑧 = (𝑛 · 𝑈)) |
40 | 28, 39 | r19.29a 3060 |
. . . 4
⊢ ((((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑚 ∈ ℤ) ∧ 𝑦 = (𝑚 · 𝑈)) → (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) |
41 | 13, 32, 33, 34, 14, 1, 35, 11, 36, 37 | archiabllem1b 29077 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑚 ∈ ℤ 𝑦 = (𝑚 · 𝑈)) |
42 | 41 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∃𝑚 ∈ ℤ 𝑦 = (𝑚 · 𝑈)) |
43 | 40, 42 | r19.29a 3060 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) |
44 | 43 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦)) |
45 | 13, 15 | isabl2 18024 |
. 2
⊢ (𝑊 ∈ Abel ↔ (𝑊 ∈ Grp ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑦(+g‘𝑊)𝑧) = (𝑧(+g‘𝑊)𝑦))) |
46 | 3, 44, 45 | sylanbrc 695 |
1
⊢ (𝜑 → 𝑊 ∈ Abel) |