Metamath Proof Explorer


Theorem rrhf

Description: If the topology of R is Hausdorff, Cauchy sequences have at most one limit, i.e. the canonical homomorphism of RR into R is a function. (Contributed by Thierry Arnoux, 2-Nov-2017)

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 rrhf φ ℝHom R : B

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 eqid topGen ran . = topGen ran .
13 1 12 3 4 5 6 7 8 9 10 11 rrhcn φ ℝHom R topGen ran . Cn K
14 uniretop = topGen ran .
15 eqid K = K
16 14 15 cnf ℝHom R topGen ran . Cn K ℝHom R : K
17 13 16 syl φ ℝHom R : K
18 nrgngp R NrmRing R NrmGrp
19 ngpxms R NrmGrp R ∞MetSp
20 7 18 19 3syl φ R ∞MetSp
21 xmstps R ∞MetSp R TopSp
22 3 4 tpsuni R TopSp B = K
23 20 21 22 3syl φ B = K
24 23 feq3d φ ℝHom R : B ℝHom R : K
25 17 24 mpbird φ ℝHom R : B