Metamath Proof Explorer

Theorem qqhucn

Description: The QQHom homomorphism is uniformly continuous. (Contributed by Thierry Arnoux, 28-Jan-2018)

Ref Expression
Hypotheses qqhucn.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
qqhucn.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
qqhucn.u ⊢ 𝑈 = ( UnifSt ‘ 𝑄 )
qqhucn.v ⊢ 𝑉 = ( metUnif ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) )
qqhucn.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
qqhucn.1 ⊢ ( 𝜑 → 𝑅 ∈ NrmRing )
qqhucn.2 ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
qqhucn.3 ⊢ ( 𝜑 → 𝑍 ∈ NrmMod )
qqhucn.4 ⊢ ( 𝜑 → ( chr ‘ 𝑅 ) = 0 )
Assertion qqhucn ( 𝜑 → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑈 Cnu 𝑉 ) )

Proof

Step Hyp Ref Expression
1 qqhucn.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 qqhucn.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
3 qqhucn.u ⊢ 𝑈 = ( UnifSt ‘ 𝑄 )
4 qqhucn.v ⊢ 𝑉 = ( metUnif ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) )
5 qqhucn.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
6 qqhucn.1 ⊢ ( 𝜑 → 𝑅 ∈ NrmRing )
7 qqhucn.2 ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
8 qqhucn.3 ⊢ ( 𝜑 → 𝑍 ∈ NrmMod )
9 qqhucn.4 ⊢ ( 𝜑 → ( chr ‘ 𝑅 ) = 0 )
10 eqid ⊢ ( /r ‘ 𝑅 ) = ( /r ‘ 𝑅 )
11 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
12 1 10 11 qqhf ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 )
13 7 9 12 syl2anc ⊢ ( 𝜑 → ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ+ )
15 nrgngp ⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
16 6 15 syl ⊢ ( 𝜑 → 𝑅 ∈ NrmGrp )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → 𝑅 ∈ NrmGrp )
18 13 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ∈ 𝐵 )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ∈ 𝐵 )
20 13 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) → ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 )
21 20 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ∈ 𝐵 )
22 eqid ⊢ ( norm ‘ 𝑅 ) = ( norm ‘ 𝑅 )
23 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
24 eqid ⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
25 22 1 23 24 ngpdsr ⊢ ( ( 𝑅 ∈ NrmGrp ∧ ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ∈ 𝐵 ∧ ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ∈ 𝐵 ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( dist ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) = ( ( norm ‘ 𝑅 ) ‘ ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ( -g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ) ) )
26 17 19 21 25 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( dist ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) = ( ( norm ‘ 𝑅 ) ‘ ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ( -g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ) ) )
27 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → 𝑞 ∈ ℚ )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → 𝑝 ∈ ℚ )
29 qsubdrg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
30 29 simpli ⊢ ℚ ∈ ( SubRing ‘ ℂfld )
31 subrgsubg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) → ℚ ∈ ( SubGrp ‘ ℂfld ) )
32 30 31 ax-mp ⊢ ℚ ∈ ( SubGrp ‘ ℂfld )
33 cnfldsub ⊢ − = ( -g ‘ ℂfld )
34 eqid ⊢ ( -g ‘ 𝑄 ) = ( -g ‘ 𝑄 )
35 33 2 34 subgsub ⊢ ( ( ℚ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ ) → ( 𝑞 − 𝑝 ) = ( 𝑞 ( -g ‘ 𝑄 ) 𝑝 ) )
36 32 35 mp3an1 ⊢ ( ( 𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ ) → ( 𝑞 − 𝑝 ) = ( 𝑞 ( -g ‘ 𝑄 ) 𝑝 ) )
37 27 28 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( 𝑞 − 𝑝 ) = ( 𝑞 ( -g ‘ 𝑄 ) 𝑝 ) )
38 37 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 − 𝑝 ) ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 ( -g ‘ 𝑄 ) 𝑝 ) ) )
39 1 10 11 2 qqhghm ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 GrpHom 𝑅 ) )
40 7 9 39 syl2anc ⊢ ( 𝜑 → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 GrpHom 𝑅 ) )
41 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 GrpHom 𝑅 ) )
42 2 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
43 42 34 23 ghmsub ⊢ ( ( ( ℚHom ‘ 𝑅 ) ∈ ( 𝑄 GrpHom 𝑅 ) ∧ 𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 ( -g ‘ 𝑄 ) 𝑝 ) ) = ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ( -g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ) )
44 41 27 28 43 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 ( -g ‘ 𝑄 ) 𝑝 ) ) = ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ( -g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ) )
45 38 44 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ( -g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ) = ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 − 𝑝 ) ) )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( norm ‘ 𝑅 ) ‘ ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ( -g ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ) ) = ( ( norm ‘ 𝑅 ) ‘ ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 − 𝑝 ) ) ) )
47 6 7 elind ⊢ ( 𝜑 → 𝑅 ∈ ( NrmRing ∩ DivRing ) )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → 𝑅 ∈ ( NrmRing ∩ DivRing ) )
49 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → 𝑍 ∈ NrmMod )
50 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( chr ‘ 𝑅 ) = 0 )
51 qsubcl ⊢ ( ( 𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ ) → ( 𝑞 − 𝑝 ) ∈ ℚ )
52 27 28 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( 𝑞 − 𝑝 ) ∈ ℚ )
53 22 5 qqhnm ⊢ ( ( ( 𝑅 ∈ ( NrmRing ∩ DivRing ) ∧ 𝑍 ∈ NrmMod ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑞 − 𝑝 ) ∈ ℚ ) → ( ( norm ‘ 𝑅 ) ‘ ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 − 𝑝 ) ) ) = ( abs ‘ ( 𝑞 − 𝑝 ) ) )
54 48 49 50 52 53 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( norm ‘ 𝑅 ) ‘ ( ( ℚHom ‘ 𝑅 ) ‘ ( 𝑞 − 𝑝 ) ) ) = ( abs ‘ ( 𝑞 − 𝑝 ) ) )
55 26 46 54 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( dist ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) = ( abs ‘ ( 𝑞 − 𝑝 ) ) )
56 19 21 ovresd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) = ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( dist ‘ 𝑅 ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) )
57 qsscn ⊢ ℚ ⊆ ℂ
58 57 28 sselid ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → 𝑝 ∈ ℂ )
59 57 27 sselid ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → 𝑞 ∈ ℂ )
60 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
61 60 cnmetdval ⊢ ( ( 𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ ) → ( 𝑝 ( abs ∘ − ) 𝑞 ) = ( abs ‘ ( 𝑝 − 𝑞 ) ) )
62 58 59 61 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( 𝑝 ( abs ∘ − ) 𝑞 ) = ( abs ‘ ( 𝑝 − 𝑞 ) ) )
63 28 27 ovresd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) = ( 𝑝 ( abs ∘ − ) 𝑞 ) )
64 59 58 abssubd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( abs ‘ ( 𝑞 − 𝑝 ) ) = ( abs ‘ ( 𝑝 − 𝑞 ) ) )
65 62 63 64 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) = ( abs ‘ ( 𝑞 − 𝑝 ) ) )
66 55 56 65 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) = ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) )
67 66 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 ↔ ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
68 67 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) ∧ 𝑞 ∈ ℚ ) → ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
69 68 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℚ ) → ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
70 69 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
72 breq2 ⊢ ( 𝑑 = 𝑒 → ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑑 ↔ ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 ) )
73 72 imbi1d ⊢ ( 𝑑 = 𝑒 → ( ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑑 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) ↔ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) ) )
74 73 2ralbidv ⊢ ( 𝑑 = 𝑒 → ( ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑑 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) ↔ ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) ) )
75 74 rspcev ⊢ ( ( 𝑒 ∈ ℝ+ ∧ ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑒 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑑 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
76 14 71 75 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑑 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
77 76 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑑 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) )
78 eqid ⊢ ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ) = ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) )
79 0z ⊢ 0 ∈ ℤ
80 zq ⊢ ( 0 ∈ ℤ → 0 ∈ ℚ )
81 ne0i ⊢ ( 0 ∈ ℚ → ℚ ≠ ∅ )
82 79 80 81 mp2b ⊢ ℚ ≠ ∅
83 82 a1i ⊢ ( 𝜑 → ℚ ≠ ∅ )
84 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
85 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
86 1 85 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
87 ne0i ⊢ ( ( 1r ‘ 𝑅 ) ∈ 𝐵 → 𝐵 ≠ ∅ )
88 7 84 86 87 4syl ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
89 cnfldxms ⊢ ℂfld ∈ ∞MetSp
90 qex ⊢ ℚ ∈ V
91 ressxms ⊢ ( ( ℂfld ∈ ∞MetSp ∧ ℚ ∈ V ) → ( ℂfld ↾s ℚ ) ∈ ∞MetSp )
92 89 90 91 mp2an ⊢ ( ℂfld ↾s ℚ ) ∈ ∞MetSp
93 2 92 eqeltri ⊢ 𝑄 ∈ ∞MetSp
94 cnfldds ⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
95 2 94 ressds ⊢ ( ℚ ∈ V → ( abs ∘ − ) = ( dist ‘ 𝑄 ) )
96 90 95 ax-mp ⊢ ( abs ∘ − ) = ( dist ‘ 𝑄 )
97 42 96 xmsxmet2 ⊢ ( 𝑄 ∈ ∞MetSp → ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ∈ ( ∞Met ‘ ℚ ) )
98 93 97 mp1i ⊢ ( 𝜑 → ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ∈ ( ∞Met ‘ ℚ ) )
99 xmetpsmet ⊢ ( ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ∈ ( ∞Met ‘ ℚ ) → ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ∈ ( PsMet ‘ ℚ ) )
100 98 99 syl ⊢ ( 𝜑 → ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ∈ ( PsMet ‘ ℚ ) )
101 ngpxms ⊢ ( 𝑅 ∈ NrmGrp → 𝑅 ∈ ∞MetSp )
102 1 24 xmsxmet2 ⊢ ( 𝑅 ∈ ∞MetSp → ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
103 6 15 101 102 4syl ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) )
104 xmetpsmet ⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ∈ ( ∞Met ‘ 𝐵 ) → ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ∈ ( PsMet ‘ 𝐵 ) )
105 103 104 syl ⊢ ( 𝜑 → ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ∈ ( PsMet ‘ 𝐵 ) )
106 78 4 83 88 100 105 metucn ⊢ ( 𝜑 → ( ( ℚHom ‘ 𝑅 ) ∈ ( ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ) Cnu 𝑉 ) ↔ ( ( ℚHom ‘ 𝑅 ) : ℚ ⟶ 𝐵 ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑝 ∈ ℚ ∀ 𝑞 ∈ ℚ ( ( 𝑝 ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) 𝑞 ) < 𝑑 → ( ( ( ℚHom ‘ 𝑅 ) ‘ 𝑝 ) ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ( ( ℚHom ‘ 𝑅 ) ‘ 𝑞 ) ) < 𝑒 ) ) ) )
107 13 77 106 mpbir2and ⊢ ( 𝜑 → ( ℚHom ‘ 𝑅 ) ∈ ( ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ) Cnu 𝑉 ) )
108 2 fveq2i ⊢ ( UnifSt ‘ 𝑄 ) = ( UnifSt ‘ ( ℂfld ↾s ℚ ) )
109 ressuss ⊢ ( ℚ ∈ V → ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) = ( ( UnifSt ‘ ℂfld ) ↾t ( ℚ × ℚ ) ) )
110 90 109 ax-mp ⊢ ( UnifSt ‘ ( ℂfld ↾s ℚ ) ) = ( ( UnifSt ‘ ℂfld ) ↾t ( ℚ × ℚ ) )
111 3 108 110 3eqtri ⊢ 𝑈 = ( ( UnifSt ‘ ℂfld ) ↾t ( ℚ × ℚ ) )
112 eqid ⊢ ( UnifSt ‘ ℂfld ) = ( UnifSt ‘ ℂfld )
113 112 cnflduss ⊢ ( UnifSt ‘ ℂfld ) = ( metUnif ‘ ( abs ∘ − ) )
114 113 oveq1i ⊢ ( ( UnifSt ‘ ℂfld ) ↾t ( ℚ × ℚ ) ) = ( ( metUnif ‘ ( abs ∘ − ) ) ↾t ( ℚ × ℚ ) )
115 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
116 xmetpsmet ⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ( abs ∘ − ) ∈ ( PsMet ‘ ℂ ) )
117 115 116 ax-mp ⊢ ( abs ∘ − ) ∈ ( PsMet ‘ ℂ )
118 restmetu ⊢ ( ( ℚ ≠ ∅ ∧ ( abs ∘ − ) ∈ ( PsMet ‘ ℂ ) ∧ ℚ ⊆ ℂ ) → ( ( metUnif ‘ ( abs ∘ − ) ) ↾t ( ℚ × ℚ ) ) = ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ) )
119 82 117 57 118 mp3an ⊢ ( ( metUnif ‘ ( abs ∘ − ) ) ↾t ( ℚ × ℚ ) ) = ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) )
120 111 114 119 3eqtri ⊢ 𝑈 = ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) )
121 120 a1i ⊢ ( 𝜑 → 𝑈 = ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ) )
122 121 oveq1d ⊢ ( 𝜑 → ( 𝑈 Cnu 𝑉 ) = ( ( metUnif ‘ ( ( abs ∘ − ) ↾ ( ℚ × ℚ ) ) ) Cnu 𝑉 ) )
123 107 122 eleqtrrd ⊢ ( 𝜑 → ( ℚHom ‘ 𝑅 ) ∈ ( 𝑈 Cnu 𝑉 ) )