| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | inss2 4238 | . . . . . . . 8
⊢ (NrmRing
∩ DivRing) ⊆ DivRing | 
| 2 | 1 | sseli 3979 | . . . . . . 7
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
→ 𝑅 ∈
DivRing) | 
| 3 | 2 | 3ad2ant1 1134 | . . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
DivRing) | 
| 4 |  | simp3 1139 | . . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(chr‘𝑅) =
0) | 
| 5 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 6 |  | eqid 2737 | . . . . . . 7
⊢
(/r‘𝑅) = (/r‘𝑅) | 
| 7 |  | eqid 2737 | . . . . . . 7
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) | 
| 8 | 5, 6, 7 | qqhf 33987 | . . . . . 6
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅):ℚ⟶(Base‘𝑅)) | 
| 9 | 3, 4, 8 | syl2anc 584 | . . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅):ℚ⟶(Base‘𝑅)) | 
| 10 |  | simpr 484 | . . . . . . 7
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) → 𝑒 ∈ ℝ+) | 
| 11 |  | qsscn 13002 | . . . . . . . . . . . . . 14
⊢ ℚ
⊆ ℂ | 
| 12 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑞 ∈ ℚ) | 
| 13 | 11, 12 | sselid 3981 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑞 ∈ ℂ) | 
| 14 |  | 0cn 11253 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℂ | 
| 15 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 16 | 15 | cnmetdval 24791 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℂ ∧ 𝑞
∈ ℂ) → (0(abs ∘ − )𝑞) = (abs‘(0 − 𝑞))) | 
| 17 | 14, 16 | mpan 690 | . . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℂ → (0(abs
∘ − )𝑞) =
(abs‘(0 − 𝑞))) | 
| 18 |  | df-neg 11495 | . . . . . . . . . . . . . . . 16
⊢ -𝑞 = (0 − 𝑞) | 
| 19 | 18 | fveq2i 6909 | . . . . . . . . . . . . . . 15
⊢
(abs‘-𝑞) =
(abs‘(0 − 𝑞)) | 
| 20 | 19 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℂ →
(abs‘-𝑞) =
(abs‘(0 − 𝑞))) | 
| 21 |  | absneg 15316 | . . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℂ →
(abs‘-𝑞) =
(abs‘𝑞)) | 
| 22 | 17, 20, 21 | 3eqtr2d 2783 | . . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℂ → (0(abs
∘ − )𝑞) =
(abs‘𝑞)) | 
| 23 | 13, 22 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0(abs ∘
− )𝑞) =
(abs‘𝑞)) | 
| 24 |  | zssq 12998 | . . . . . . . . . . . . . . 15
⊢ ℤ
⊆ ℚ | 
| 25 |  | 0z 12624 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ | 
| 26 | 24, 25 | sselii 3980 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℚ | 
| 27 | 26 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 0 ∈
ℚ) | 
| 28 | 27, 12 | ovresd 7600 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) = (0(abs ∘ − )𝑞)) | 
| 29 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(norm‘𝑅) =
(norm‘𝑅) | 
| 30 |  | qqhcn.z | . . . . . . . . . . . . . 14
⊢ 𝑍 = (ℤMod‘𝑅) | 
| 31 | 29, 30 | qqhnm 33991 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑞 ∈ ℚ) →
((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞)) = (abs‘𝑞)) | 
| 32 | 31 | adantlr 715 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞)) = (abs‘𝑞)) | 
| 33 | 23, 28, 32 | 3eqtr4d 2787 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) = ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞))) | 
| 34 | 9 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(ℚHom‘𝑅):ℚ⟶(Base‘𝑅)) | 
| 35 | 34, 27 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘0) ∈ (Base‘𝑅)) | 
| 36 | 34, 12 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘𝑞) ∈ (Base‘𝑅)) | 
| 37 | 35, 36 | ovresd 7600 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) = (((ℚHom‘𝑅)‘0)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞))) | 
| 38 |  | inss1 4237 | . . . . . . . . . . . . . . . . 17
⊢ (NrmRing
∩ DivRing) ⊆ NrmRing | 
| 39 | 38 | sseli 3979 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
→ 𝑅 ∈
NrmRing) | 
| 40 | 39 | 3ad2ant1 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
NrmRing) | 
| 41 | 40 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ NrmRing) | 
| 42 |  | nrgngp 24683 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) | 
| 43 | 41, 42 | syl 17 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ NrmGrp) | 
| 44 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(-g‘𝑅) = (-g‘𝑅) | 
| 45 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(dist‘𝑅) =
(dist‘𝑅) | 
| 46 | 29, 5, 44, 45 | ngpdsr 24618 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ NrmGrp ∧
((ℚHom‘𝑅)‘0) ∈ (Base‘𝑅) ∧ ((ℚHom‘𝑅)‘𝑞) ∈ (Base‘𝑅)) → (((ℚHom‘𝑅)‘0)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)))) | 
| 47 | 43, 35, 36, 46 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘0)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)))) | 
| 48 | 3 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ DivRing) | 
| 49 | 4 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (chr‘𝑅) = 0) | 
| 50 | 5, 6, 7 | qqh0 33985 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
((ℚHom‘𝑅)‘0) = (0g‘𝑅)) | 
| 51 | 48, 49, 50 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘0) = (0g‘𝑅)) | 
| 52 | 51 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)) = (((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)(0g‘𝑅))) | 
| 53 |  | ngpgrp 24612 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈ Grp) | 
| 54 | 43, 53 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ Grp) | 
| 55 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 56 | 5, 55, 44 | grpsubid1 19043 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Grp ∧
((ℚHom‘𝑅)‘𝑞) ∈ (Base‘𝑅)) → (((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)(0g‘𝑅)) = ((ℚHom‘𝑅)‘𝑞)) | 
| 57 | 54, 36, 56 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)(0g‘𝑅)) = ((ℚHom‘𝑅)‘𝑞)) | 
| 58 | 52, 57 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0)) = ((ℚHom‘𝑅)‘𝑞)) | 
| 59 | 58 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘0))) = ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞))) | 
| 60 | 37, 47, 59 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘((ℚHom‘𝑅)‘𝑞))) | 
| 61 | 33, 60 | eqtr4d 2780 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → (0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) = (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞))) | 
| 62 | 61 | breq1d 5153 | . . . . . . . . 9
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑒 ↔ (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 63 | 62 | biimpd 229 | . . . . . . . 8
⊢ ((((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) ∧ 𝑞 ∈ ℚ) → ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 64 | 63 | ralrimiva 3146 | . . . . . . 7
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) → ∀𝑞 ∈ ℚ ((0((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 65 |  | breq2 5147 | . . . . . . . 8
⊢ (𝑑 = 𝑒 → ((0((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑑 ↔ (0((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑒)) | 
| 66 | 65 | rspceaimv 3628 | . . . . . . 7
⊢ ((𝑒 ∈ ℝ+
∧ ∀𝑞 ∈
ℚ ((0((abs ∘ − ) ↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) → ∃𝑑 ∈ ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 67 | 10, 64, 66 | syl2anc 584 | . . . . . 6
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
𝑒 ∈
ℝ+) → ∃𝑑 ∈ ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 68 | 67 | ralrimiva 3146 | . . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
∀𝑒 ∈
ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 69 |  | qqhcn.q | . . . . . . . 8
⊢ 𝑄 = (ℂfld
↾s ℚ) | 
| 70 |  | cnfldxms 24797 | . . . . . . . . 9
⊢
ℂfld ∈ ∞MetSp | 
| 71 |  | qex 13003 | . . . . . . . . 9
⊢ ℚ
∈ V | 
| 72 |  | ressxms 24538 | . . . . . . . . 9
⊢
((ℂfld ∈ ∞MetSp ∧ ℚ ∈ V)
→ (ℂfld ↾s ℚ) ∈
∞MetSp) | 
| 73 | 70, 71, 72 | mp2an 692 | . . . . . . . 8
⊢
(ℂfld ↾s ℚ) ∈
∞MetSp | 
| 74 | 69, 73 | eqeltri 2837 | . . . . . . 7
⊢ 𝑄 ∈
∞MetSp | 
| 75 | 69 | qrngbas 27663 | . . . . . . . 8
⊢ ℚ =
(Base‘𝑄) | 
| 76 |  | cnfldds 21376 | . . . . . . . . . 10
⊢ (abs
∘ − ) = (dist‘ℂfld) | 
| 77 | 69, 76 | ressds 17454 | . . . . . . . . 9
⊢ (ℚ
∈ V → (abs ∘ − ) = (dist‘𝑄)) | 
| 78 | 71, 77 | ax-mp 5 | . . . . . . . 8
⊢ (abs
∘ − ) = (dist‘𝑄) | 
| 79 | 75, 78 | xmsxmet2 24469 | . . . . . . 7
⊢ (𝑄 ∈ ∞MetSp →
((abs ∘ − ) ↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ)) | 
| 80 | 74, 79 | mp1i 13 | . . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((abs ∘ − ) ↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ)) | 
| 81 |  | ngpxms 24614 | . . . . . . . . 9
⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈
∞MetSp) | 
| 82 | 39, 42, 81 | 3syl 18 | . . . . . . . 8
⊢ (𝑅 ∈ (NrmRing ∩ DivRing)
→ 𝑅 ∈
∞MetSp) | 
| 83 | 82 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
∞MetSp) | 
| 84 | 5, 45 | xmsxmet2 24469 | . . . . . . 7
⊢ (𝑅 ∈ ∞MetSp →
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) ∈
(∞Met‘(Base‘𝑅))) | 
| 85 | 83, 84 | syl 17 | . . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) ∈
(∞Met‘(Base‘𝑅))) | 
| 86 | 26 | a1i 11 | . . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) → 0
∈ ℚ) | 
| 87 |  | qqhcn.j | . . . . . . . . 9
⊢ 𝐽 = (TopOpen‘𝑄) | 
| 88 | 78 | reseq1i 5993 | . . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (ℚ × ℚ)) = ((dist‘𝑄) ↾ (ℚ ×
ℚ)) | 
| 89 | 87, 75, 88 | xmstopn 24461 | . . . . . . . 8
⊢ (𝑄 ∈ ∞MetSp →
𝐽 = (MetOpen‘((abs
∘ − ) ↾ (ℚ × ℚ)))) | 
| 90 | 74, 89 | ax-mp 5 | . . . . . . 7
⊢ 𝐽 = (MetOpen‘((abs ∘
− ) ↾ (ℚ × ℚ))) | 
| 91 |  | eqid 2737 | . . . . . . 7
⊢
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))) = (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))) | 
| 92 | 90, 91 | metcnp 24554 | . . . . . 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‘𝑅)‘𝑞)) < 𝑒)))) | 
| 93 | 80, 85, 86, 92 | syl3anc 1373 | . . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((ℚHom‘𝑅)
∈ ((𝐽 CnP
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))‘0) ↔
((ℚHom‘𝑅):ℚ⟶(Base‘𝑅) ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑞 ∈ ℚ ((0((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘0)((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))((ℚHom‘𝑅)‘𝑞)) < 𝑒)))) | 
| 94 | 9, 68, 93 | mpbir2and 713 | . . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
((𝐽 CnP
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))‘0)) | 
| 95 |  | qqhcn.k | . . . . . . . 8
⊢ 𝐾 = (TopOpen‘𝑅) | 
| 96 |  | eqid 2737 | . . . . . . . 8
⊢
((dist‘𝑅)
↾ ((Base‘𝑅)
× (Base‘𝑅))) =
((dist‘𝑅) ↾
((Base‘𝑅) ×
(Base‘𝑅))) | 
| 97 | 95, 5, 96 | xmstopn 24461 | . . . . . . 7
⊢ (𝑅 ∈ ∞MetSp →
𝐾 =
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))) | 
| 98 | 83, 97 | syl 17 | . . . . . 6
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝐾 =
(MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))))) | 
| 99 | 98 | oveq2d 7447 | . . . . 5
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(𝐽 CnP 𝐾) = (𝐽 CnP (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))) | 
| 100 | 99 | fveq1d 6908 | . . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((𝐽 CnP 𝐾)‘0) = ((𝐽 CnP (MetOpen‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))‘0)) | 
| 101 | 94, 100 | eleqtrrd 2844 | . . 3
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
((𝐽 CnP 𝐾)‘0)) | 
| 102 |  | cnfldtgp 24893 | . . . . . 6
⊢
ℂfld ∈ TopGrp | 
| 103 |  | qsubdrg 21437 | . . . . . . . 8
⊢ (ℚ
∈ (SubRing‘ℂfld) ∧ (ℂfld
↾s ℚ) ∈ DivRing) | 
| 104 | 103 | simpli 483 | . . . . . . 7
⊢ ℚ
∈ (SubRing‘ℂfld) | 
| 105 |  | subrgsubg 20577 | . . . . . . 7
⊢ (ℚ
∈ (SubRing‘ℂfld) → ℚ ∈
(SubGrp‘ℂfld)) | 
| 106 | 104, 105 | ax-mp 5 | . . . . . 6
⊢ ℚ
∈ (SubGrp‘ℂfld) | 
| 107 | 69 | subgtgp 24113 | . . . . . 6
⊢
((ℂfld ∈ TopGrp ∧ ℚ ∈
(SubGrp‘ℂfld)) → 𝑄 ∈ TopGrp) | 
| 108 | 102, 106,
107 | mp2an 692 | . . . . 5
⊢ 𝑄 ∈ TopGrp | 
| 109 |  | tgptmd 24087 | . . . . 5
⊢ (𝑄 ∈ TopGrp → 𝑄 ∈ TopMnd) | 
| 110 | 108, 109 | mp1i 13 | . . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑄 ∈
TopMnd) | 
| 111 |  | nrgtrg 24711 | . . . . 5
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈
TopRing) | 
| 112 |  | trgtmd2 24177 | . . . . 5
⊢ (𝑅 ∈ TopRing → 𝑅 ∈ TopMnd) | 
| 113 | 40, 111, 112 | 3syl 18 | . . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
𝑅 ∈
TopMnd) | 
| 114 | 5, 6, 7, 69 | qqhghm 33989 | . . . . 5
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) | 
| 115 | 3, 4, 114 | syl2anc 584 | . . . 4
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) | 
| 116 | 75, 87, 95 | ghmcnp 24123 | . . . 4
⊢ ((𝑄 ∈ TopMnd ∧ 𝑅 ∈ TopMnd ∧
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) → ((ℚHom‘𝑅) ∈ ((𝐽 CnP 𝐾)‘0) ↔ (0 ∈ ℚ ∧
(ℚHom‘𝑅) ∈
(𝐽 Cn 𝐾)))) | 
| 117 | 110, 113,
115, 116 | syl3anc 1373 | . . 3
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
((ℚHom‘𝑅)
∈ ((𝐽 CnP 𝐾)‘0) ↔ (0 ∈
ℚ ∧ (ℚHom‘𝑅) ∈ (𝐽 Cn 𝐾)))) | 
| 118 | 101, 117 | mpbid 232 | . 2
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(0 ∈ ℚ ∧ (ℚHom‘𝑅) ∈ (𝐽 Cn 𝐾))) | 
| 119 | 118 | simprd 495 | 1
⊢ ((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝐽 Cn 𝐾)) |