| Step | Hyp | Ref
| Expression |
| 1 | | isofld 33332 |
. . . 4
⊢ (𝑊 ∈ oField ↔ (𝑊 ∈ Field ∧ 𝑊 ∈ oRing)) |
| 2 | 1 | simprbi 496 |
. . 3
⊢ (𝑊 ∈ oField → 𝑊 ∈ oRing) |
| 3 | | orngogrp 33331 |
. . 3
⊢ (𝑊 ∈ oRing → 𝑊 ∈ oGrp) |
| 4 | | isarchiofld.b |
. . . 4
⊢ 𝐵 = (Base‘𝑊) |
| 5 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 6 | | isarchiofld.l |
. . . 4
⊢ < =
(lt‘𝑊) |
| 7 | | eqid 2737 |
. . . 4
⊢
(.g‘𝑊) = (.g‘𝑊) |
| 8 | 4, 5, 6, 7 | isarchi3 33194 |
. . 3
⊢ (𝑊 ∈ oGrp → (𝑊 ∈ Archi ↔
∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)))) |
| 9 | 2, 3, 8 | 3syl 18 |
. 2
⊢ (𝑊 ∈ oField → (𝑊 ∈ Archi ↔
∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)))) |
| 10 | | orngring 33330 |
. . . . . . 7
⊢ (𝑊 ∈ oRing → 𝑊 ∈ Ring) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(1r‘𝑊) = (1r‘𝑊) |
| 12 | 4, 11 | ringidcl 20262 |
. . . . . . 7
⊢ (𝑊 ∈ Ring →
(1r‘𝑊)
∈ 𝐵) |
| 13 | 2, 10, 12 | 3syl 18 |
. . . . . 6
⊢ (𝑊 ∈ oField →
(1r‘𝑊)
∈ 𝐵) |
| 14 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑦 = (1r‘𝑊) →
((0g‘𝑊)
<
𝑦 ↔
(0g‘𝑊)
<
(1r‘𝑊))) |
| 15 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = (1r‘𝑊) → (𝑛(.g‘𝑊)𝑦) = (𝑛(.g‘𝑊)(1r‘𝑊))) |
| 16 | 15 | breq2d 5155 |
. . . . . . . . . 10
⊢ (𝑦 = (1r‘𝑊) → (𝑥 < (𝑛(.g‘𝑊)𝑦) ↔ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 17 | 16 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑦 = (1r‘𝑊) → (∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 18 | 14, 17 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑦 = (1r‘𝑊) →
(((0g‘𝑊)
<
𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) ↔ ((0g‘𝑊) <
(1r‘𝑊)
→ ∃𝑛 ∈
ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊))))) |
| 19 | 18 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑦 = (1r‘𝑊) → (∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) ↔ ∀𝑥 ∈ 𝐵 ((0g‘𝑊) <
(1r‘𝑊)
→ ∃𝑛 ∈
ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊))))) |
| 20 | 19 | rspcv 3618 |
. . . . . 6
⊢
((1r‘𝑊) ∈ 𝐵 → (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) → ∀𝑥 ∈ 𝐵 ((0g‘𝑊) <
(1r‘𝑊)
→ ∃𝑛 ∈
ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊))))) |
| 21 | 13, 20 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ oField →
(∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) → ∀𝑥 ∈ 𝐵 ((0g‘𝑊) <
(1r‘𝑊)
→ ∃𝑛 ∈
ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊))))) |
| 22 | 5, 11, 6 | ofldlt1 33343 |
. . . . . . 7
⊢ (𝑊 ∈ oField →
(0g‘𝑊)
<
(1r‘𝑊)) |
| 23 | | pm5.5 361 |
. . . . . . 7
⊢
((0g‘𝑊) <
(1r‘𝑊)
→ (((0g‘𝑊) <
(1r‘𝑊)
→ ∃𝑛 ∈
ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊))) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 24 | 22, 23 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ oField →
(((0g‘𝑊)
<
(1r‘𝑊)
→ ∃𝑛 ∈
ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊))) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 25 | 24 | ralbidv 3178 |
. . . . 5
⊢ (𝑊 ∈ oField →
(∀𝑥 ∈ 𝐵 ((0g‘𝑊) <
(1r‘𝑊)
→ ∃𝑛 ∈
ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊))) ↔ ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 26 | 21, 25 | sylibd 239 |
. . . 4
⊢ (𝑊 ∈ oField →
(∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) → ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 27 | 2, 10 | syl 17 |
. . . . . . . 8
⊢ (𝑊 ∈ oField → 𝑊 ∈ Ring) |
| 28 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
| 29 | | isarchiofld.h |
. . . . . . . . 9
⊢ 𝐻 = (ℤRHom‘𝑊) |
| 30 | 29, 7, 11 | zrhmulg 21520 |
. . . . . . . 8
⊢ ((𝑊 ∈ Ring ∧ 𝑛 ∈ ℤ) → (𝐻‘𝑛) = (𝑛(.g‘𝑊)(1r‘𝑊))) |
| 31 | 27, 28, 30 | syl2an 596 |
. . . . . . 7
⊢ ((𝑊 ∈ oField ∧ 𝑛 ∈ ℕ) → (𝐻‘𝑛) = (𝑛(.g‘𝑊)(1r‘𝑊))) |
| 32 | 31 | breq2d 5155 |
. . . . . 6
⊢ ((𝑊 ∈ oField ∧ 𝑛 ∈ ℕ) → (𝑥 < (𝐻‘𝑛) ↔ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 33 | 32 | rexbidva 3177 |
. . . . 5
⊢ (𝑊 ∈ oField →
(∃𝑛 ∈ ℕ
𝑥 < (𝐻‘𝑛) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 34 | 33 | ralbidv 3178 |
. . . 4
⊢ (𝑊 ∈ oField →
(∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛) ↔ ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)(1r‘𝑊)))) |
| 35 | 26, 34 | sylibrd 259 |
. . 3
⊢ (𝑊 ∈ oField →
(∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) → ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛))) |
| 36 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑊 ∈ oField |
| 37 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛) |
| 38 | 36, 37 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) |
| 39 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑦 ∈ 𝐵 |
| 40 | 38, 39 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑥((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ 𝑦 ∈ 𝐵) |
| 41 | 27 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → 𝑊 ∈ Ring) |
| 42 | | simplrr 778 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → 𝑥 ∈ 𝐵) |
| 43 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → 𝑦 ∈ 𝐵) |
| 44 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → (0g‘𝑊) < 𝑦) |
| 45 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → 𝑊 ∈ oField) |
| 46 | | ringgrp 20235 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Ring → 𝑊 ∈ Grp) |
| 47 | 4, 5 | grpidcl 18983 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Grp →
(0g‘𝑊)
∈ 𝐵) |
| 48 | 41, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → (0g‘𝑊) ∈ 𝐵) |
| 49 | 6 | pltne 18379 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ oField ∧
(0g‘𝑊)
∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((0g‘𝑊) < 𝑦 → (0g‘𝑊) ≠ 𝑦)) |
| 50 | 45, 48, 43, 49 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → ((0g‘𝑊) < 𝑦 → (0g‘𝑊) ≠ 𝑦)) |
| 51 | 44, 50 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → (0g‘𝑊) ≠ 𝑦) |
| 52 | 51 | necomd 2996 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → 𝑦 ≠ (0g‘𝑊)) |
| 53 | 1 | simplbi 497 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ oField → 𝑊 ∈ Field) |
| 54 | | isfld 20740 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Field ↔ (𝑊 ∈ DivRing ∧ 𝑊 ∈ CRing)) |
| 55 | 54 | simplbi 497 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Field → 𝑊 ∈
DivRing) |
| 56 | 53, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ oField → 𝑊 ∈
DivRing) |
| 57 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Unit‘𝑊) =
(Unit‘𝑊) |
| 58 | 4, 57, 5 | drngunit 20734 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ DivRing → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ (0g‘𝑊)))) |
| 59 | 45, 56, 58 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ (0g‘𝑊)))) |
| 60 | 43, 52, 59 | mpbir2and 713 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → 𝑦 ∈ (Unit‘𝑊)) |
| 61 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(/r‘𝑊) = (/r‘𝑊) |
| 62 | 4, 57, 61 | dvrcl 20404 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ (Unit‘𝑊)) → (𝑥(/r‘𝑊)𝑦) ∈ 𝐵) |
| 63 | 41, 42, 60, 62 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → (𝑥(/r‘𝑊)𝑦) ∈ 𝐵) |
| 64 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) → ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) |
| 65 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑥 < (𝐻‘𝑛) ↔ 𝑧 < (𝐻‘𝑛))) |
| 66 | 65 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛) ↔ ∃𝑛 ∈ ℕ 𝑧 < (𝐻‘𝑛))) |
| 67 | 66 | cbvralvw 3237 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛) ↔ ∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑧 < (𝐻‘𝑛)) |
| 68 | 64, 67 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) → ∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑧 < (𝐻‘𝑛)) |
| 69 | 68 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → ∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑧 < (𝐻‘𝑛)) |
| 70 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥(/r‘𝑊)𝑦) → (𝑧 < (𝐻‘𝑛) ↔ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛))) |
| 71 | 70 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥(/r‘𝑊)𝑦) → (∃𝑛 ∈ ℕ 𝑧 < (𝐻‘𝑛) ↔ ∃𝑛 ∈ ℕ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛))) |
| 72 | 71 | rspcv 3618 |
. . . . . . . . . 10
⊢ ((𝑥(/r‘𝑊)𝑦) ∈ 𝐵 → (∀𝑧 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑧 < (𝐻‘𝑛) → ∃𝑛 ∈ ℕ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛))) |
| 73 | 63, 69, 72 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → ∃𝑛 ∈ ℕ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) |
| 74 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑊) = (.r‘𝑊) |
| 75 | | simp-4l 783 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑊 ∈ oField) |
| 76 | 75, 2 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑊 ∈ oRing) |
| 77 | 75, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑊 ∈ Ring) |
| 78 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) |
| 79 | 78 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑥 ∈ 𝐵) |
| 80 | 78 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑦 ∈ 𝐵) |
| 81 | | simpllr 776 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (0g‘𝑊) < 𝑦) |
| 82 | 77, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (0g‘𝑊) ∈ 𝐵) |
| 83 | 75, 82, 80, 49 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → ((0g‘𝑊) < 𝑦 → (0g‘𝑊) ≠ 𝑦)) |
| 84 | 81, 83 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (0g‘𝑊) ≠ 𝑦) |
| 85 | 84 | necomd 2996 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑦 ≠ (0g‘𝑊)) |
| 86 | 75, 56, 58 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ (0g‘𝑊)))) |
| 87 | 80, 85, 86 | mpbir2and 713 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑦 ∈ (Unit‘𝑊)) |
| 88 | 77, 79, 87, 62 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝑥(/r‘𝑊)𝑦) ∈ 𝐵) |
| 89 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑛 ∈ ℕ) |
| 90 | 75, 89, 31 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝐻‘𝑛) = (𝑛(.g‘𝑊)(1r‘𝑊))) |
| 91 | 77, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑊 ∈ Grp) |
| 92 | 89, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑛 ∈ ℤ) |
| 93 | 77, 12 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (1r‘𝑊) ∈ 𝐵) |
| 94 | 4, 7 | mulgcl 19109 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧
(1r‘𝑊)
∈ 𝐵) → (𝑛(.g‘𝑊)(1r‘𝑊)) ∈ 𝐵) |
| 95 | 91, 92, 93, 94 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝑛(.g‘𝑊)(1r‘𝑊)) ∈ 𝐵) |
| 96 | 90, 95 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝐻‘𝑛) ∈ 𝐵) |
| 97 | 75, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑊 ∈ DivRing) |
| 98 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) |
| 99 | 4, 74, 5, 76, 88, 96, 80, 6, 97, 98, 81 | orngrmullt 33338 |
. . . . . . . . . . . . 13
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → ((𝑥(/r‘𝑊)𝑦)(.r‘𝑊)𝑦) < ((𝐻‘𝑛)(.r‘𝑊)𝑦)) |
| 100 | 4, 57, 61, 74 | dvrcan1 20409 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ (Unit‘𝑊)) → ((𝑥(/r‘𝑊)𝑦)(.r‘𝑊)𝑦) = 𝑥) |
| 101 | 77, 79, 87, 100 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → ((𝑥(/r‘𝑊)𝑦)(.r‘𝑊)𝑦) = 𝑥) |
| 102 | 90 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → ((𝐻‘𝑛)(.r‘𝑊)𝑦) = ((𝑛(.g‘𝑊)(1r‘𝑊))(.r‘𝑊)𝑦)) |
| 103 | 4, 7, 74 | mulgass2 20306 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Ring ∧ (𝑛 ∈ ℤ ∧
(1r‘𝑊)
∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑛(.g‘𝑊)(1r‘𝑊))(.r‘𝑊)𝑦) = (𝑛(.g‘𝑊)((1r‘𝑊)(.r‘𝑊)𝑦))) |
| 104 | 77, 92, 93, 80, 103 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → ((𝑛(.g‘𝑊)(1r‘𝑊))(.r‘𝑊)𝑦) = (𝑛(.g‘𝑊)((1r‘𝑊)(.r‘𝑊)𝑦))) |
| 105 | 4, 74, 11 | ringlidm 20266 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Ring ∧ 𝑦 ∈ 𝐵) → ((1r‘𝑊)(.r‘𝑊)𝑦) = 𝑦) |
| 106 | 77, 80, 105 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → ((1r‘𝑊)(.r‘𝑊)𝑦) = 𝑦) |
| 107 | 106 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → (𝑛(.g‘𝑊)((1r‘𝑊)(.r‘𝑊)𝑦)) = (𝑛(.g‘𝑊)𝑦)) |
| 108 | 102, 104,
107 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → ((𝐻‘𝑛)(.r‘𝑊)𝑦) = (𝑛(.g‘𝑊)𝑦)) |
| 109 | 99, 101, 108 | 3brtr3d 5174 |
. . . . . . . . . . . 12
⊢
(((((𝑊 ∈ oField
∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛)) → 𝑥 < (𝑛(.g‘𝑊)𝑦)) |
| 110 | 109 | ex 412 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ oField ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) → ((𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛) → 𝑥 < (𝑛(.g‘𝑊)𝑦))) |
| 111 | 110 | reximdva 3168 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ oField ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → (∃𝑛 ∈ ℕ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦))) |
| 112 | 111 | adantllr 719 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → (∃𝑛 ∈ ℕ (𝑥(/r‘𝑊)𝑦) < (𝐻‘𝑛) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦))) |
| 113 | 73, 112 | mpd 15 |
. . . . . . . 8
⊢ ((((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) ∧ (0g‘𝑊) < 𝑦) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) |
| 114 | 113 | ex 412 |
. . . . . . 7
⊢ (((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦))) |
| 115 | 114 | expr 456 |
. . . . . 6
⊢ (((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝐵 → ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)))) |
| 116 | 40, 115 | ralrimi 3257 |
. . . . 5
⊢ (((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦))) |
| 117 | 116 | ralrimiva 3146 |
. . . 4
⊢ ((𝑊 ∈ oField ∧
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛)) → ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦))) |
| 118 | 117 | ex 412 |
. . 3
⊢ (𝑊 ∈ oField →
(∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛) → ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)))) |
| 119 | 35, 118 | impbid 212 |
. 2
⊢ (𝑊 ∈ oField →
(∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((0g‘𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g‘𝑊)𝑦)) ↔ ∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛))) |
| 120 | 9, 119 | bitrd 279 |
1
⊢ (𝑊 ∈ oField → (𝑊 ∈ Archi ↔
∀𝑥 ∈ 𝐵 ∃𝑛 ∈ ℕ 𝑥 < (𝐻‘𝑛))) |