Metamath Proof Explorer


Theorem rrhcn

Description: If the topology of R is Hausdorff, and R is a complete uniform space, then the canonical homomorphism from the real numbers to R is continuous. (Contributed by Thierry Arnoux, 17-Jan-2018)

Ref Expression
Hypotheses rrhf.d D = dist R B × B
rrhf.j J = topGen ran .
rrhf.b B = Base R
rrhf.k K = TopOpen R
rrhf.z Z = ℤMod R
rrhf.1 φ R DivRing
rrhf.2 φ R NrmRing
rrhf.3 φ Z NrmMod
rrhf.4 φ chr R = 0
rrhf.5 φ R CUnifSp
rrhf.6 φ UnifSt R = metUnif D
Assertion rrhcn φ ℝHom R J Cn K

Proof

Step Hyp Ref Expression
1 rrhf.d D = dist R B × B
2 rrhf.j J = topGen ran .
3 rrhf.b B = Base R
4 rrhf.k K = TopOpen R
5 rrhf.z Z = ℤMod R
6 rrhf.1 φ R DivRing
7 rrhf.2 φ R NrmRing
8 rrhf.3 φ Z NrmMod
9 rrhf.4 φ chr R = 0
10 rrhf.5 φ R CUnifSp
11 rrhf.6 φ UnifSt R = metUnif D
12 nrgngp R NrmRing R NrmGrp
13 ngpxms R NrmGrp R ∞MetSp
14 7 12 13 3syl φ R ∞MetSp
15 xmstps R ∞MetSp R TopSp
16 14 15 syl φ R TopSp
17 2 4 rrhval R TopSp ℝHom R = J CnExt K ℚHom R
18 16 17 syl φ ℝHom R = J CnExt K ℚHom R
19 rebase = Base fld
20 retopn topGen ran . = TopOpen fld
21 2 20 eqtri J = TopOpen fld
22 eqid UnifSt fld = UnifSt fld
23 df-refld fld = fld 𝑠
24 23 oveq1i fld 𝑠 = fld 𝑠 𝑠
25 reex V
26 qssre
27 ressabs V fld 𝑠 𝑠 = fld 𝑠
28 25 26 27 mp2an fld 𝑠 𝑠 = fld 𝑠
29 24 28 eqtr2i fld 𝑠 = fld 𝑠
30 29 fveq2i UnifSt fld 𝑠 = UnifSt fld 𝑠
31 eqid UnifSt R = UnifSt R
32 recms fld CMetSp
33 cmsms fld CMetSp fld MetSp
34 mstps fld MetSp fld TopSp
35 32 33 34 mp2b fld TopSp
36 35 a1i φ fld TopSp
37 recusp fld CUnifSp
38 cuspusp fld CUnifSp fld UnifSp
39 37 38 mp1i φ fld UnifSp
40 4 3 1 xmstopn R ∞MetSp K = MetOpen D
41 14 40 syl φ K = MetOpen D
42 3 1 xmsxmet R ∞MetSp D ∞Met B
43 eqid MetOpen D = MetOpen D
44 43 methaus D ∞Met B MetOpen D Haus
45 14 42 44 3syl φ MetOpen D Haus
46 41 45 eqeltrd φ K Haus
47 26 a1i φ
48 eqid fld 𝑠 = fld 𝑠
49 eqid UnifSt fld 𝑠 = UnifSt fld 𝑠
50 1 fveq2i metUnif D = metUnif dist R B × B
51 3 48 49 50 5 7 6 8 9 qqhucn φ ℚHom R UnifSt fld 𝑠 uCn metUnif D
52 11 eqcomd φ metUnif D = UnifSt R
53 52 oveq2d φ UnifSt fld 𝑠 uCn metUnif D = UnifSt fld 𝑠 uCn UnifSt R
54 51 53 eleqtrd φ ℚHom R UnifSt fld 𝑠 uCn UnifSt R
55 2 fveq2i cls J = cls topGen ran .
56 55 fveq1i cls J = cls topGen ran .
57 qdensere cls topGen ran . =
58 56 57 eqtri cls J =
59 58 a1i φ cls J =
60 19 3 21 4 22 30 31 36 39 16 10 46 47 54 59 ucnextcn φ J CnExt K ℚHom R J Cn K
61 18 60 eqeltrd φ ℝHom R J Cn K