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 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑝 ∈ β„š ) β†’ ( ( β„šHom β€˜ 𝑅 ) β€˜ 𝑝 ) ∈ 𝐡 )
19 18 adantr ⊒ ( ( ( πœ‘ ∧ 𝑝 ∈ β„š ) ∧ π‘ž ∈ β„š ) β†’ ( ( β„šHom β€˜ 𝑅 ) β€˜ 𝑝 ) ∈ 𝐡 )
20 13 adantr ⊒ ( ( πœ‘ ∧ 𝑝 ∈ β„š ) β†’ ( β„šHom β€˜ 𝑅 ) : β„š ⟢ 𝐡 )
21 20 ffvelcdmda ⊒ ( ( ( πœ‘ ∧ 𝑝 ∈ β„š ) ∧ π‘ž ∈ β„š ) β†’ ( ( β„š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 𝑉 ) )