| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | qqhucn.2 | . . . 4
⊢ (𝜑 → 𝑅 ∈ DivRing) | 
| 2 |  | qqhucn.4 | . . . 4
⊢ (𝜑 → (chr‘𝑅) = 0) | 
| 3 |  | qqhucn.b | . . . . 5
⊢ 𝐵 = (Base‘𝑅) | 
| 4 |  | eqid 2737 | . . . . 5
⊢
(/r‘𝑅) = (/r‘𝑅) | 
| 5 |  | eqid 2737 | . . . . 5
⊢
(ℤRHom‘𝑅) = (ℤRHom‘𝑅) | 
| 6 | 3, 4, 5 | qqhf 33987 | . . . 4
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅):ℚ⟶𝐵) | 
| 7 | 1, 2, 6 | syl2anc 584 | . . 3
⊢ (𝜑 → (ℚHom‘𝑅):ℚ⟶𝐵) | 
| 8 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) | 
| 9 |  | qqhucn.1 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ NrmRing) | 
| 10 |  | nrgngp 24683 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ NrmGrp) | 
| 12 | 11 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ NrmGrp) | 
| 13 | 7 | ffvelcdmda 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ ℚ) →
((ℚHom‘𝑅)‘𝑝) ∈ 𝐵) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘𝑝) ∈ 𝐵) | 
| 15 | 7 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ ℚ) →
(ℚHom‘𝑅):ℚ⟶𝐵) | 
| 16 | 15 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘𝑞) ∈ 𝐵) | 
| 17 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(norm‘𝑅) =
(norm‘𝑅) | 
| 18 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(-g‘𝑅) = (-g‘𝑅) | 
| 19 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(dist‘𝑅) =
(dist‘𝑅) | 
| 20 | 17, 3, 18, 19 | ngpdsr 24618 | . . . . . . . . . . . . 13
⊢ ((𝑅 ∈ NrmGrp ∧
((ℚHom‘𝑅)‘𝑝) ∈ 𝐵 ∧ ((ℚHom‘𝑅)‘𝑞) ∈ 𝐵) → (((ℚHom‘𝑅)‘𝑝)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘𝑝)))) | 
| 21 | 12, 14, 16, 20 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑝)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞)) = ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘𝑝)))) | 
| 22 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → 𝑞 ∈ ℚ) | 
| 23 |  | simplr 769 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → 𝑝 ∈ ℚ) | 
| 24 |  | qsubdrg 21437 | . . . . . . . . . . . . . . . . . . 19
⊢ (ℚ
∈ (SubRing‘ℂfld) ∧ (ℂfld
↾s ℚ) ∈ DivRing) | 
| 25 | 24 | simpli 483 | . . . . . . . . . . . . . . . . . 18
⊢ ℚ
∈ (SubRing‘ℂfld) | 
| 26 |  | subrgsubg 20577 | . . . . . . . . . . . . . . . . . 18
⊢ (ℚ
∈ (SubRing‘ℂfld) → ℚ ∈
(SubGrp‘ℂfld)) | 
| 27 | 25, 26 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ ℚ
∈ (SubGrp‘ℂfld) | 
| 28 |  | cnfldsub 21410 | . . . . . . . . . . . . . . . . . 18
⊢  −
= (-g‘ℂfld) | 
| 29 |  | qqhucn.q | . . . . . . . . . . . . . . . . . 18
⊢ 𝑄 = (ℂfld
↾s ℚ) | 
| 30 |  | eqid 2737 | . . . . . . . . . . . . . . . . . 18
⊢
(-g‘𝑄) = (-g‘𝑄) | 
| 31 | 28, 29, 30 | subgsub 19156 | . . . . . . . . . . . . . . . . 17
⊢ ((ℚ
∈ (SubGrp‘ℂfld) ∧ 𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 − 𝑝) = (𝑞(-g‘𝑄)𝑝)) | 
| 32 | 27, 31 | mp3an1 1450 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 − 𝑝) = (𝑞(-g‘𝑄)𝑝)) | 
| 33 | 22, 23, 32 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (𝑞 − 𝑝) = (𝑞(-g‘𝑄)𝑝)) | 
| 34 | 33 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘(𝑞 − 𝑝)) = ((ℚHom‘𝑅)‘(𝑞(-g‘𝑄)𝑝))) | 
| 35 | 3, 4, 5, 29 | qqhghm 33989 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ DivRing ∧
(chr‘𝑅) = 0) →
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) | 
| 36 | 1, 2, 35 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℚHom‘𝑅) ∈ (𝑄 GrpHom 𝑅)) | 
| 37 | 36 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
(ℚHom‘𝑅) ∈
(𝑄 GrpHom 𝑅)) | 
| 38 | 29 | qrngbas 27663 | . . . . . . . . . . . . . . . 16
⊢ ℚ =
(Base‘𝑄) | 
| 39 | 38, 30, 18 | ghmsub 19242 | . . . . . . . . . . . . . . 15
⊢
(((ℚHom‘𝑅) ∈ (𝑄 GrpHom 𝑅) ∧ 𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((ℚHom‘𝑅)‘(𝑞(-g‘𝑄)𝑝)) = (((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘𝑝))) | 
| 40 | 37, 22, 23, 39 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
((ℚHom‘𝑅)‘(𝑞(-g‘𝑄)𝑝)) = (((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘𝑝))) | 
| 41 | 34, 40 | eqtr2d 2778 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘𝑝)) = ((ℚHom‘𝑅)‘(𝑞 − 𝑝))) | 
| 42 | 41 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → ((norm‘𝑅)‘(((ℚHom‘𝑅)‘𝑞)(-g‘𝑅)((ℚHom‘𝑅)‘𝑝))) = ((norm‘𝑅)‘((ℚHom‘𝑅)‘(𝑞 − 𝑝)))) | 
| 43 | 9, 1 | elind 4200 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ (NrmRing ∩
DivRing)) | 
| 44 | 43 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → 𝑅 ∈ (NrmRing ∩
DivRing)) | 
| 45 |  | qqhucn.3 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ NrmMod) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → 𝑍 ∈ NrmMod) | 
| 47 | 2 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (chr‘𝑅) = 0) | 
| 48 |  | qsubcl 13010 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 − 𝑝) ∈ ℚ) | 
| 49 | 22, 23, 48 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (𝑞 − 𝑝) ∈ ℚ) | 
| 50 |  | qqhucn.z | . . . . . . . . . . . . . 14
⊢ 𝑍 = (ℤMod‘𝑅) | 
| 51 | 17, 50 | qqhnm 33991 | . . . . . . . . . . . . 13
⊢ (((𝑅 ∈ (NrmRing ∩ DivRing)
∧ 𝑍 ∈ NrmMod ∧
(chr‘𝑅) = 0) ∧
(𝑞 − 𝑝) ∈ ℚ) →
((norm‘𝑅)‘((ℚHom‘𝑅)‘(𝑞 − 𝑝))) = (abs‘(𝑞 − 𝑝))) | 
| 52 | 44, 46, 47, 49, 51 | syl31anc 1375 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → ((norm‘𝑅)‘((ℚHom‘𝑅)‘(𝑞 − 𝑝))) = (abs‘(𝑞 − 𝑝))) | 
| 53 | 21, 42, 52 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑝)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞)) = (abs‘(𝑞 − 𝑝))) | 
| 54 | 14, 16 | ovresd 7600 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) = (((ℚHom‘𝑅)‘𝑝)(dist‘𝑅)((ℚHom‘𝑅)‘𝑞))) | 
| 55 |  | qsscn 13002 | . . . . . . . . . . . . . 14
⊢ ℚ
⊆ ℂ | 
| 56 | 55, 23 | sselid 3981 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → 𝑝 ∈ ℂ) | 
| 57 | 55, 22 | sselid 3981 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → 𝑞 ∈ ℂ) | 
| 58 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 59 | 58 | cnmetdval 24791 | . . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ) → (𝑝(abs ∘ − )𝑞) = (abs‘(𝑝 − 𝑞))) | 
| 60 | 56, 57, 59 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (𝑝(abs ∘ − )𝑞) = (abs‘(𝑝 − 𝑞))) | 
| 61 | 23, 22 | ovresd 7600 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) =
(𝑝(abs ∘ −
)𝑞)) | 
| 62 | 57, 56 | abssubd 15492 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (abs‘(𝑞 − 𝑝)) = (abs‘(𝑝 − 𝑞))) | 
| 63 | 60, 61, 62 | 3eqtr4d 2787 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) =
(abs‘(𝑞 − 𝑝))) | 
| 64 | 53, 54, 63 | 3eqtr4rd 2788 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → (𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) =
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞))) | 
| 65 | 64 | breq1d 5153 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑒 ↔
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 66 | 65 | biimpd 229 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℚ) ∧ 𝑞 ∈ ℚ) → ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑒 →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 67 | 66 | ralrimiva 3146 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℚ) → ∀𝑞 ∈ ℚ ((𝑝((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 68 | 67 | ralrimiva 3146 | . . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ ℚ ∀𝑞 ∈ ℚ ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑒 →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 69 | 68 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑝 ∈ ℚ
∀𝑞 ∈ ℚ
((𝑝((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 70 |  | breq2 5147 | . . . . . . . 8
⊢ (𝑑 = 𝑒 → ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑑 ↔ (𝑝((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑒)) | 
| 71 | 70 | imbi1d 341 | . . . . . . 7
⊢ (𝑑 = 𝑒 → (((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑑 →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒) ↔ ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑒 →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒))) | 
| 72 | 71 | 2ralbidv 3221 | . . . . . 6
⊢ (𝑑 = 𝑒 → (∀𝑝 ∈ ℚ ∀𝑞 ∈ ℚ ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑑 →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒) ↔ ∀𝑝 ∈ ℚ ∀𝑞 ∈ ℚ ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑒 →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒))) | 
| 73 | 72 | rspcev 3622 | . . . . 5
⊢ ((𝑒 ∈ ℝ+
∧ ∀𝑝 ∈
ℚ ∀𝑞 ∈
ℚ ((𝑝((abs ∘
− ) ↾ (ℚ × ℚ))𝑞) < 𝑒 → (((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) → ∃𝑑 ∈ ℝ+ ∀𝑝 ∈ ℚ ∀𝑞 ∈ ℚ ((𝑝((abs ∘ − ) ↾
(ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 74 | 8, 69, 73 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑝 ∈ ℚ ∀𝑞 ∈ ℚ ((𝑝((abs ∘ − ) ↾ (ℚ
× ℚ))𝑞) <
𝑑 →
(((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 75 | 74 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑝 ∈ ℚ
∀𝑞 ∈ ℚ
((𝑝((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)) | 
| 76 |  | eqid 2737 | . . . 4
⊢
(metUnif‘((abs ∘ − ) ↾ (ℚ ×
ℚ))) = (metUnif‘((abs ∘ − ) ↾ (ℚ ×
ℚ))) | 
| 77 |  | qqhucn.v | . . . 4
⊢ 𝑉 =
(metUnif‘((dist‘𝑅) ↾ (𝐵 × 𝐵))) | 
| 78 |  | 0z 12624 | . . . . . 6
⊢ 0 ∈
ℤ | 
| 79 |  | zq 12996 | . . . . . 6
⊢ (0 ∈
ℤ → 0 ∈ ℚ) | 
| 80 |  | ne0i 4341 | . . . . . 6
⊢ (0 ∈
ℚ → ℚ ≠ ∅) | 
| 81 | 78, 79, 80 | mp2b 10 | . . . . 5
⊢ ℚ
≠ ∅ | 
| 82 | 81 | a1i 11 | . . . 4
⊢ (𝜑 → ℚ ≠
∅) | 
| 83 |  | drngring 20736 | . . . . 5
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) | 
| 84 |  | eqid 2737 | . . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 85 | 3, 84 | ringidcl 20262 | . . . . 5
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) | 
| 86 |  | ne0i 4341 | . . . . 5
⊢
((1r‘𝑅) ∈ 𝐵 → 𝐵 ≠ ∅) | 
| 87 | 1, 83, 85, 86 | 4syl 19 | . . . 4
⊢ (𝜑 → 𝐵 ≠ ∅) | 
| 88 |  | cnfldxms 24797 | . . . . . . . 8
⊢
ℂfld ∈ ∞MetSp | 
| 89 |  | qex 13003 | . . . . . . . 8
⊢ ℚ
∈ V | 
| 90 |  | ressxms 24538 | . . . . . . . 8
⊢
((ℂfld ∈ ∞MetSp ∧ ℚ ∈ V)
→ (ℂfld ↾s ℚ) ∈
∞MetSp) | 
| 91 | 88, 89, 90 | mp2an 692 | . . . . . . 7
⊢
(ℂfld ↾s ℚ) ∈
∞MetSp | 
| 92 | 29, 91 | eqeltri 2837 | . . . . . 6
⊢ 𝑄 ∈
∞MetSp | 
| 93 |  | cnfldds 21376 | . . . . . . . . 9
⊢ (abs
∘ − ) = (dist‘ℂfld) | 
| 94 | 29, 93 | ressds 17454 | . . . . . . . 8
⊢ (ℚ
∈ V → (abs ∘ − ) = (dist‘𝑄)) | 
| 95 | 89, 94 | ax-mp 5 | . . . . . . 7
⊢ (abs
∘ − ) = (dist‘𝑄) | 
| 96 | 38, 95 | xmsxmet2 24469 | . . . . . 6
⊢ (𝑄 ∈ ∞MetSp →
((abs ∘ − ) ↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ)) | 
| 97 | 92, 96 | mp1i 13 | . . . . 5
⊢ (𝜑 → ((abs ∘ − )
↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ)) | 
| 98 |  | xmetpsmet 24358 | . . . . 5
⊢ (((abs
∘ − ) ↾ (ℚ × ℚ)) ∈
(∞Met‘ℚ) → ((abs ∘ − ) ↾ (ℚ
× ℚ)) ∈ (PsMet‘ℚ)) | 
| 99 | 97, 98 | syl 17 | . . . 4
⊢ (𝜑 → ((abs ∘ − )
↾ (ℚ × ℚ)) ∈
(PsMet‘ℚ)) | 
| 100 |  | ngpxms 24614 | . . . . . 6
⊢ (𝑅 ∈ NrmGrp → 𝑅 ∈
∞MetSp) | 
| 101 | 3, 19 | xmsxmet2 24469 | . . . . . 6
⊢ (𝑅 ∈ ∞MetSp →
((dist‘𝑅) ↾
(𝐵 × 𝐵)) ∈
(∞Met‘𝐵)) | 
| 102 | 9, 10, 100, 101 | 4syl 19 | . . . . 5
⊢ (𝜑 → ((dist‘𝑅) ↾ (𝐵 × 𝐵)) ∈ (∞Met‘𝐵)) | 
| 103 |  | xmetpsmet 24358 | . . . . 5
⊢
(((dist‘𝑅)
↾ (𝐵 × 𝐵)) ∈
(∞Met‘𝐵) →
((dist‘𝑅) ↾
(𝐵 × 𝐵)) ∈ (PsMet‘𝐵)) | 
| 104 | 102, 103 | syl 17 | . . . 4
⊢ (𝜑 → ((dist‘𝑅) ↾ (𝐵 × 𝐵)) ∈ (PsMet‘𝐵)) | 
| 105 | 76, 77, 82, 87, 99, 104 | metucn 24584 | . . 3
⊢ (𝜑 → ((ℚHom‘𝑅) ∈ ((metUnif‘((abs
∘ − ) ↾ (ℚ × ℚ))) Cnu𝑉) ↔
((ℚHom‘𝑅):ℚ⟶𝐵 ∧ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑝 ∈ ℚ
∀𝑞 ∈ ℚ
((𝑝((abs ∘ − )
↾ (ℚ × ℚ))𝑞) < 𝑑 → (((ℚHom‘𝑅)‘𝑝)((dist‘𝑅) ↾ (𝐵 × 𝐵))((ℚHom‘𝑅)‘𝑞)) < 𝑒)))) | 
| 106 | 7, 75, 105 | mpbir2and 713 | . 2
⊢ (𝜑 → (ℚHom‘𝑅) ∈ ((metUnif‘((abs
∘ − ) ↾ (ℚ × ℚ))) Cnu𝑉)) | 
| 107 |  | qqhucn.u | . . . . . 6
⊢ 𝑈 = (UnifSt‘𝑄) | 
| 108 | 29 | fveq2i 6909 | . . . . . 6
⊢
(UnifSt‘𝑄) =
(UnifSt‘(ℂfld ↾s
ℚ)) | 
| 109 |  | ressuss 24271 | . . . . . . 7
⊢ (ℚ
∈ V → (UnifSt‘(ℂfld ↾s
ℚ)) = ((UnifSt‘ℂfld) ↾t (ℚ
× ℚ))) | 
| 110 | 89, 109 | ax-mp 5 | . . . . . 6
⊢
(UnifSt‘(ℂfld ↾s ℚ)) =
((UnifSt‘ℂfld) ↾t (ℚ ×
ℚ)) | 
| 111 | 107, 108,
110 | 3eqtri 2769 | . . . . 5
⊢ 𝑈 =
((UnifSt‘ℂfld) ↾t (ℚ ×
ℚ)) | 
| 112 |  | eqid 2737 | . . . . . . 7
⊢
(UnifSt‘ℂfld) =
(UnifSt‘ℂfld) | 
| 113 | 112 | cnflduss 25390 | . . . . . 6
⊢
(UnifSt‘ℂfld) = (metUnif‘(abs ∘
− )) | 
| 114 | 113 | oveq1i 7441 | . . . . 5
⊢
((UnifSt‘ℂfld) ↾t (ℚ
× ℚ)) = ((metUnif‘(abs ∘ − )) ↾t
(ℚ × ℚ)) | 
| 115 |  | cnxmet 24793 | . . . . . . 7
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 116 |  | xmetpsmet 24358 | . . . . . . 7
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → (abs ∘ −
) ∈ (PsMet‘ℂ)) | 
| 117 | 115, 116 | ax-mp 5 | . . . . . 6
⊢ (abs
∘ − ) ∈ (PsMet‘ℂ) | 
| 118 |  | restmetu 24583 | . . . . . 6
⊢ ((ℚ
≠ ∅ ∧ (abs ∘ − ) ∈ (PsMet‘ℂ) ∧
ℚ ⊆ ℂ) → ((metUnif‘(abs ∘ − ))
↾t (ℚ × ℚ)) = (metUnif‘((abs ∘
− ) ↾ (ℚ × ℚ)))) | 
| 119 | 81, 117, 55, 118 | mp3an 1463 | . . . . 5
⊢
((metUnif‘(abs ∘ − )) ↾t (ℚ
× ℚ)) = (metUnif‘((abs ∘ − ) ↾ (ℚ
× ℚ))) | 
| 120 | 111, 114,
119 | 3eqtri 2769 | . . . 4
⊢ 𝑈 = (metUnif‘((abs ∘
− ) ↾ (ℚ × ℚ))) | 
| 121 | 120 | a1i 11 | . . 3
⊢ (𝜑 → 𝑈 = (metUnif‘((abs ∘ − )
↾ (ℚ × ℚ)))) | 
| 122 | 121 | oveq1d 7446 | . 2
⊢ (𝜑 → (𝑈 Cnu𝑉) = ((metUnif‘((abs ∘ − )
↾ (ℚ × ℚ))) Cnu𝑉)) | 
| 123 | 106, 122 | eleqtrrd 2844 | 1
⊢ (𝜑 → (ℚHom‘𝑅) ∈ (𝑈 Cnu𝑉)) |