Step | Hyp | Ref
| Expression |
1 | | inss2 3796 |
. . . . . . . 8
⊢ (NrmRing
∩ DivRing) ⊆ DivRing |
2 | 1 | sseli 3564 |
. . . . . . 7
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
→ 𝑅 ∈
DivRing) |
3 | 2 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
DivRing) |
4 | | simp3 1056 |
. . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(chr‘𝑅) =
0) |
5 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | | eqid 2610 |
. . . . . . 7
⊢
(/r‘𝑅) = (/r‘𝑅) |
7 | | eqid 2610 |
. . . . . . 7
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) |
8 | 5, 6, 7 | qqhf 29358 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅):ℚ⟶(Base‘𝑅)) |
9 | 3, 4, 8 | syl2anc 691 |
. . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅):ℚ⟶(Base‘𝑅)) |
10 | | simpr 476 |
. . . . . . 7
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) → 𝑒 ∈ ℝ+) |
11 | | qsscn 11675 |
. . . . . . . . . . . . . 14
⊢ ℚ
⊆ ℂ |
12 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑞 ∈ ℚ) |
13 | 11, 12 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑞 ∈ ℂ) |
14 | | 0cn 9911 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℂ |
15 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) = (abs ∘ − ) |
16 | 15 | cnmetdval 22384 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℂ ∧ 𝑞
∈ ℂ) → (0(abs ∘ − )𝑞) = (abs‘(0 − 𝑞))) |
17 | 14, 16 | mpan 702 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℂ → (0(abs
∘ − )𝑞) =
(abs‘(0 − 𝑞))) |
18 | | df-neg 10148 |
. . . . . . . . . . . . . . . 16
⊢ -𝑞 = (0 − 𝑞) |
19 | 18 | fveq2i 6106 |
. . . . . . . . . . . . . . 15
⊢
(abs‘-𝑞) =
(abs‘(0 − 𝑞)) |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℂ →
(abs‘-𝑞) =
(abs‘(0 − 𝑞))) |
21 | | absneg 13865 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℂ →
(abs‘-𝑞) =
(abs‘𝑞)) |
22 | 17, 20, 21 | 3eqtr2d 2650 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℂ → (0(abs
∘ − )𝑞) =
(abs‘𝑞)) |
23 | 13, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0(abs ∘
− )𝑞) =
(abs‘𝑞)) |
24 | | zssq 11671 |
. . . . . . . . . . . . . . 15
⊢ ℤ
⊆ ℚ |
25 | | 0z 11265 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
26 | 24, 25 | sselii 3565 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℚ |
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 0 ∈
ℚ) |
28 | 27, 12 | ovresd 6699 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) = (0(abs ∘ − )𝑞)) |
29 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(norm‘𝑅) =
(norm‘𝑅) |
30 | | qqhcn.z |
. . . . . . . . . . . . . 14
⊢ 𝑍 = (ℤMod‘𝑅) |
31 | 29, 30 | qqhnm 29362 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞)) = (abs‘𝑞)) |
32 | 31 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞)) = (abs‘𝑞)) |
33 | 23, 28, 32 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) = ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞))) |
34 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(ℚHom‘𝑅):ℚ⟶(Base‘𝑅)) |
35 | 34, 27 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘0) ∈ (Base‘𝑅)) |
36 | 34, 12 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘𝑞) ∈ (Base‘𝑅)) |
37 | 35, 36 | ovresd 6699 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) = (((ℚHom‘𝑅)‘0)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞))) |
38 | | inss1 3795 |
. . . . . . . . . . . . . . . . 17
⊢ (NrmRing
∩ DivRing) ⊆ NrmRing |
39 | 38 | sseli 3564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
→ 𝑅 ∈
NrmRing) |
40 | 39 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
NrmRing) |
41 | 40 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ NrmRing) |
42 | | nrgngp 22276 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ NrmGrp) |
44 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(-g‘𝑅) = (-g‘𝑅) |
45 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(dist‘𝑅) =
(dist‘𝑅) |
46 | 29, 5, 44, 45 | ngpdsr 22219 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ NrmGrp ∧
((ℚHom‘𝑅)‘0) ∈ (Base‘𝑅) ∧ ((ℚHom‘𝑅)‘𝑞) ∈ (Base‘𝑅)) → (((ℚHom‘𝑅)‘0)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)))) |
47 | 43, 35, 36, 46 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘0)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)))) |
48 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ DivRing) |
49 | 4 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (chr‘𝑅) = 0) |
50 | 5, 6, 7 | qqh0 29356 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
((ℚHom‘𝑅)‘0) = (0g‘𝑅)) |
51 | 48, 49, 50 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘0) = (0g‘𝑅)) |
52 | 51 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)) = (((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)(0g‘𝑅))) |
53 | | ngpgrp 22213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ Grp) |
54 | 43, 53 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ Grp) |
55 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) = (0g‘𝑅) |
56 | 5, 55, 44 | grpsubid1 17323 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Grp ∧
((ℚHom‘𝑅)‘𝑞) ∈ (Base‘𝑅)) → (((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)(0g‘𝑅)) = ((ℚHom‘𝑅)‘𝑞)) |
57 | 54, 36, 56 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)(0g‘𝑅)) = ((ℚHom‘𝑅)‘𝑞)) |
58 | 52, 57 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)) = ((ℚHom‘𝑅)‘𝑞)) |
59 | 58 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0))) = ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞))) |
60 | 37, 47, 59 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞))) |
61 | 33, 60 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) = (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞))) |
62 | 61 | breq1d 4593 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑒 ↔ (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) |
63 | 62 | biimpd 218 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) |
64 | 63 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) → ∀𝑞 ∈ ℚ ((0((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) |
65 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑒 → ((0((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑑 ↔ (0((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑒)) |
66 | 65 | imbi1d 330 |
. . . . . . . . 9
⊢ (𝑑 = 𝑒 → (((0((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒) ↔ ((0((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒))) |
67 | 66 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑑 = 𝑒 → (∀𝑞 ∈ ℚ ((0((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒) ↔ ∀𝑞 ∈ ℚ ((0((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒))) |
68 | 67 | rspcev 3282 |
. . . . . . 7
⊢ ((𝑒 ∈ ℝ+
∧ ∀𝑞 ∈
ℚ ((0((abs ∘ − ) ↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) → ∃𝑑 ∈ ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) |
69 | 10, 64, 68 | syl2anc 691 |
. . . . . 6
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) → ∃𝑑 ∈ ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) |
70 | 69 | ralrimiva 2949 |
. . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) |
71 | | qqhcn.q |
. . . . . . . 8
⊢ 𝑄 = (ℂfld
↾s ℚ) |
72 | | cnfldxms 22390 |
. . . . . . . . 9
⊢
ℂfld ∈ ∞MetSp |
73 | | qex 11676 |
. . . . . . . . 9
⊢ ℚ
∈ V |
74 | | ressxms 22140 |
. . . . . . . . 9
⊢
((ℂfld ∈ ∞MetSp ∧ ℚ ∈ V)
→ (ℂfld ↾s ℚ) ∈
∞MetSp) |
75 | 72, 73, 74 | mp2an 704 |
. . . . . . . 8
⊢
(ℂfld ↾s ℚ) ∈
∞MetSp |
76 | 71, 75 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑄 ∈
∞MetSp |
77 | 71 | qrngbas 25108 |
. . . . . . . 8
⊢ ℚ =
(Base‘𝑄) |
78 | | cnfldds 19577 |
. . . . . . . . . 10
⊢ (abs
∘ − ) = (dist‘ℂfld) |
79 | 71, 78 | ressds 15896 |
. . . . . . . . 9
⊢ (ℚ
∈ V → (abs ∘ − ) = (dist‘𝑄)) |
80 | 73, 79 | ax-mp 5 |
. . . . . . . 8
⊢ (abs
∘ − ) = (dist‘𝑄) |
81 | 77, 80 | xmsxmet2 22074 |
. . . . . . 7
⊢ (𝑄 ∈ ∞MetSp →
((abs ∘ − ) ↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ)) |
82 | 76, 81 | mp1i 13 |
. . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((abs ∘ − ) ↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ)) |
83 | | ngpxms 22215 |
. . . . . . . . 9
⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈
∞MetSp) |
84 | 39, 42, 83 | 3syl 18 |
. . . . . . . 8
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
→ 𝑅 ∈
∞MetSp) |
85 | 84 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
∞MetSp) |
86 | 5, 45 | xmsxmet2 22074 |
. . . . . . 7
⊢ (𝑅 ∈ ∞MetSp →
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) ∈
(∞Met‘(Base‘𝑅))) |
87 | 85, 86 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) ∈
(∞Met‘(Base‘𝑅))) |
88 | 26 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) → 0
∈ ℚ) |
89 | | qqhcn.j |
. . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝑄) |
90 | 80 | reseq1i 5313 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℚ × ℚ)) = ((dist‘𝑄) ↾ (ℚ ×
ℚ)) |
91 | 89, 77, 90 | xmstopn 22066 |
. . . . . . . 8
⊢ (𝑄 ∈ ∞MetSp →
𝐽 = (MetOpen‘((abs
∘ − ) ↾ (ℚ × ℚ)))) |
92 | 76, 91 | ax-mp 5 |
. . . . . . 7
⊢ 𝐽 = (MetOpen‘((abs ∘
− ) ↾ (ℚ × ℚ))) |
93 | | eqid 2610 |
. . . . . . 7
⊢
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))) = (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))) |
94 | 92, 93 | metcnp 22156 |
. . . . . 6
⊢ ((((abs
∘ − ) ↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ) ∧ ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) ∈
(∞Met‘(Base‘𝑅)) ∧ 0 ∈ ℚ) →
((ℚHom‘𝑅)
∈ ((𝐽 CnP
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))‘0) ↔
((ℚHom‘𝑅):ℚ⟶(Base‘𝑅) ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)))) |
95 | 82, 87, 88, 94 | syl3anc 1318 |
. . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((ℚHom‘𝑅)
∈ ((𝐽 CnP
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))‘0) ↔
((ℚHom‘𝑅):ℚ⟶(Base‘𝑅) ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)))) |
96 | 9, 70, 95 | mpbir2and 959 |
. . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
((𝐽 CnP
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))‘0)) |
97 | | qqhcn.k |
. . . . . . . 8
⊢ 𝐾 = (TopOpen‘𝑅) |
98 | | eqid 2610 |
. . . . . . . 8
⊢
((dist‘𝑅)
↾ ((Base‘𝑅)
× (Base‘𝑅))) =
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) |
99 | 97, 5, 98 | xmstopn 22066 |
. . . . . . 7
⊢ (𝑅 ∈ ∞MetSp →
𝐾 =
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))) |
100 | 85, 99 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝐾 =
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))) |
101 | 100 | oveq2d 6565 |
. . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(𝐽 CnP 𝐾) = (𝐽 CnP (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))) |
102 | 101 | fveq1d 6105 |
. . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((𝐽 CnP 𝐾)‘0) = ((𝐽 CnP (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))‘0)) |
103 | 96, 102 | eleqtrrd 2691 |
. . 3
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
((𝐽 CnP 𝐾)‘0)) |
104 | | cnfldtgp 22480 |
. . . . . 6
⊢
ℂfld ∈ TopGrp |
105 | | qsubdrg 19617 |
. . . . . . . 8
⊢ (ℚ
∈ (SubRing‘ℂfld) ∧ (ℂfld
↾s ℚ) ∈ DivRing) |
106 | 105 | simpli 473 |
. . . . . . 7
⊢ ℚ
∈ (SubRing‘ℂfld) |
107 | | subrgsubg 18609 |
. . . . . . 7
⊢ (ℚ
∈ (SubRing‘ℂfld) → ℚ ∈
(SubGrp‘ℂfld)) |
108 | 106, 107 | ax-mp 5 |
. . . . . 6
⊢ ℚ
∈ (SubGrp‘ℂfld) |
109 | 71 | subgtgp 21719 |
. . . . . 6
⊢
((ℂfld ∈ TopGrp ∧ ℚ ∈
(SubGrp‘ℂfld)) → 𝑄 ∈ TopGrp) |
110 | 104, 108,
109 | mp2an 704 |
. . . . 5
⊢ 𝑄 ∈ TopGrp |
111 | | tgptmd 21693 |
. . . . 5
⊢ (𝑄 ∈ TopGrp → 𝑄 ∈ TopMnd) |
112 | 110, 111 | mp1i 13 |
. . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑄 ∈
TopMnd) |
113 | | nrgtrg 22304 |
. . . . 5
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈
TopRing) |
114 | | trgtmd2 21782 |
. . . . 5
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopMnd) |
115 | 40, 113, 114 | 3syl 18 |
. . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
TopMnd) |
116 | 5, 6, 7, 71 | qqhghm 29360 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) |
117 | 3, 4, 116 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) |
118 | 77, 89, 97 | ghmcnp 21728 |
. . . 4
⊢ ((𝑄 ∈ TopMnd ∧ 𝑅 ∈ TopMnd ∧
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) → ((ℚHom‘𝑅) ∈ ((𝐽 CnP 𝐾)‘0) ↔ (0 ∈ ℚ ∧
(ℚHom‘𝑅) ∈
(𝐽 Cn 𝐾)))) |
119 | 112, 115,
117, 118 | syl3anc 1318 |
. . 3
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((ℚHom‘𝑅)
∈ ((𝐽 CnP 𝐾)‘0) ↔ (0 ∈
ℚ ∧ (ℚHom‘𝑅) ∈ (𝐽 Cn 𝐾)))) |
120 | 103, 119 | mpbid 221 |
. 2
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(0 ∈ ℚ ∧ (ℚHom‘𝑅) ∈ (𝐽 Cn 𝐾))) |
121 | 120 | simprd 478 |
1
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝐽 Cn 𝐾)) |