Metamath Proof Explorer


Theorem qqhucn

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

Ref Expression
Hypotheses qqhucn.b B=BaseR
qqhucn.q Q=fld𝑠
qqhucn.u U=UnifStQ
qqhucn.v V=metUnifdistRB×B
qqhucn.z Z=ℤModR
qqhucn.1 φRNrmRing
qqhucn.2 φRDivRing
qqhucn.3 φZNrmMod
qqhucn.4 φchrR=0
Assertion qqhucn φℚHomRUuCnV

Proof

Step Hyp Ref Expression
1 qqhucn.b B=BaseR
2 qqhucn.q Q=fld𝑠
3 qqhucn.u U=UnifStQ
4 qqhucn.v V=metUnifdistRB×B
5 qqhucn.z Z=ℤModR
6 qqhucn.1 φRNrmRing
7 qqhucn.2 φRDivRing
8 qqhucn.3 φZNrmMod
9 qqhucn.4 φchrR=0
10 eqid /rR=/rR
11 eqid ℤRHomR=ℤRHomR
12 1 10 11 qqhf RDivRingchrR=0ℚHomR:B
13 7 9 12 syl2anc φℚHomR:B
14 simpr φe+e+
15 nrgngp RNrmRingRNrmGrp
16 6 15 syl φRNrmGrp
17 16 ad2antrr φpqRNrmGrp
18 13 ffvelrnda φpℚHomRpB
19 18 adantr φpqℚHomRpB
20 13 adantr φpℚHomR:B
21 20 ffvelrnda φpqℚHomRqB
22 eqid normR=normR
23 eqid -R=-R
24 eqid distR=distR
25 22 1 23 24 ngpdsr RNrmGrpℚHomRpBℚHomRqBℚHomRpdistRℚHomRq=normRℚHomRq-RℚHomRp
26 17 19 21 25 syl3anc φpqℚHomRpdistRℚHomRq=normRℚHomRq-RℚHomRp
27 simpr φpqq
28 simplr φpqp
29 qsubdrg SubRingfldfld𝑠DivRing
30 29 simpli SubRingfld
31 subrgsubg SubRingfldSubGrpfld
32 30 31 ax-mp SubGrpfld
33 cnfldsub =-fld
34 eqid -Q=-Q
35 33 2 34 subgsub SubGrpfldqpqp=q-Qp
36 32 35 mp3an1 qpqp=q-Qp
37 27 28 36 syl2anc φpqqp=q-Qp
38 37 fveq2d φpqℚHomRqp=ℚHomRq-Qp
39 1 10 11 2 qqhghm RDivRingchrR=0ℚHomRQGrpHomR
40 7 9 39 syl2anc φℚHomRQGrpHomR
41 40 ad2antrr φpqℚHomRQGrpHomR
42 2 qrngbas =BaseQ
43 42 34 23 ghmsub ℚHomRQGrpHomRqpℚHomRq-Qp=ℚHomRq-RℚHomRp
44 41 27 28 43 syl3anc φpqℚHomRq-Qp=ℚHomRq-RℚHomRp
45 38 44 eqtr2d φpqℚHomRq-RℚHomRp=ℚHomRqp
46 45 fveq2d φpqnormRℚHomRq-RℚHomRp=normRℚHomRqp
47 6 7 elind φRNrmRingDivRing
48 47 ad2antrr φpqRNrmRingDivRing
49 8 ad2antrr φpqZNrmMod
50 9 ad2antrr φpqchrR=0
51 qsubcl qpqp
52 27 28 51 syl2anc φpqqp
53 22 5 qqhnm RNrmRingDivRingZNrmModchrR=0qpnormRℚHomRqp=qp
54 48 49 50 52 53 syl31anc φpqnormRℚHomRqp=qp
55 26 46 54 3eqtrd φpqℚHomRpdistRℚHomRq=qp
56 19 21 ovresd φpqℚHomRpdistRB×BℚHomRq=ℚHomRpdistRℚHomRq
57 qsscn
58 57 28 sselid φpqp
59 57 27 sselid φpqq
60 eqid abs=abs
61 60 cnmetdval pqpabsq=pq
62 58 59 61 syl2anc φpqpabsq=pq
63 28 27 ovresd φpqpabs×q=pabsq
64 59 58 abssubd φpqqp=pq
65 62 63 64 3eqtr4d φpqpabs×q=qp
66 55 56 65 3eqtr4rd φpqpabs×q=ℚHomRpdistRB×BℚHomRq
67 66 breq1d φpqpabs×q<eℚHomRpdistRB×BℚHomRq<e
68 67 biimpd φpqpabs×q<eℚHomRpdistRB×BℚHomRq<e
69 68 ralrimiva φpqpabs×q<eℚHomRpdistRB×BℚHomRq<e
70 69 ralrimiva φpqpabs×q<eℚHomRpdistRB×BℚHomRq<e
71 70 adantr φe+pqpabs×q<eℚHomRpdistRB×BℚHomRq<e
72 breq2 d=epabs×q<dpabs×q<e
73 72 imbi1d d=epabs×q<dℚHomRpdistRB×BℚHomRq<epabs×q<eℚHomRpdistRB×BℚHomRq<e
74 73 2ralbidv d=epqpabs×q<dℚHomRpdistRB×BℚHomRq<epqpabs×q<eℚHomRpdistRB×BℚHomRq<e
75 74 rspcev e+pqpabs×q<eℚHomRpdistRB×BℚHomRq<ed+pqpabs×q<dℚHomRpdistRB×BℚHomRq<e
76 14 71 75 syl2anc φe+d+pqpabs×q<dℚHomRpdistRB×BℚHomRq<e
77 76 ralrimiva φe+d+pqpabs×q<dℚHomRpdistRB×BℚHomRq<e
78 eqid metUnifabs×=metUnifabs×
79 0z 0
80 zq 00
81 ne0i 0
82 79 80 81 mp2b
83 82 a1i φ
84 drngring RDivRingRRing
85 eqid 1R=1R
86 1 85 ringidcl RRing1RB
87 ne0i 1RBB
88 7 84 86 87 4syl φB
89 cnfldxms fld∞MetSp
90 qex V
91 ressxms fld∞MetSpVfld𝑠∞MetSp
92 89 90 91 mp2an fld𝑠∞MetSp
93 2 92 eqeltri Q∞MetSp
94 cnfldds abs=distfld
95 2 94 ressds Vabs=distQ
96 90 95 ax-mp abs=distQ
97 42 96 xmsxmet2 Q∞MetSpabs×∞Met
98 93 97 mp1i φabs×∞Met
99 xmetpsmet abs×∞Metabs×PsMet
100 98 99 syl φabs×PsMet
101 ngpxms RNrmGrpR∞MetSp
102 1 24 xmsxmet2 R∞MetSpdistRB×B∞MetB
103 6 15 101 102 4syl φdistRB×B∞MetB
104 xmetpsmet distRB×B∞MetBdistRB×BPsMetB
105 103 104 syl φdistRB×BPsMetB
106 78 4 83 88 100 105 metucn φℚHomRmetUnifabs×uCnVℚHomR:Be+d+pqpabs×q<dℚHomRpdistRB×BℚHomRq<e
107 13 77 106 mpbir2and φℚHomRmetUnifabs×uCnV
108 2 fveq2i UnifStQ=UnifStfld𝑠
109 ressuss VUnifStfld𝑠=UnifStfld𝑡×
110 90 109 ax-mp UnifStfld𝑠=UnifStfld𝑡×
111 3 108 110 3eqtri U=UnifStfld𝑡×
112 eqid UnifStfld=UnifStfld
113 112 cnflduss UnifStfld=metUnifabs
114 113 oveq1i UnifStfld𝑡×=metUnifabs𝑡×
115 cnxmet abs∞Met
116 xmetpsmet abs∞MetabsPsMet
117 115 116 ax-mp absPsMet
118 restmetu absPsMetmetUnifabs𝑡×=metUnifabs×
119 82 117 57 118 mp3an metUnifabs𝑡×=metUnifabs×
120 111 114 119 3eqtri U=metUnifabs×
121 120 a1i φU=metUnifabs×
122 121 oveq1d φUuCnV=metUnifabs×uCnV
123 107 122 eleqtrrd φℚHomRUuCnV