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 𝐷 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
rrhf.j 𝐽 = ( topGen ‘ ran (,) )
rrhf.b 𝐵 = ( Base ‘ 𝑅 )
rrhf.k 𝐾 = ( TopOpen ‘ 𝑅 )
rrhf.z 𝑍 = ( ℤMod ‘ 𝑅 )
rrhf.1 ( 𝜑𝑅 ∈ DivRing )
rrhf.2 ( 𝜑𝑅 ∈ NrmRing )
rrhf.3 ( 𝜑𝑍 ∈ NrmMod )
rrhf.4 ( 𝜑 → ( chr ‘ 𝑅 ) = 0 )
rrhf.5 ( 𝜑𝑅 ∈ CUnifSp )
rrhf.6 ( 𝜑 → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) )
Assertion rrhf ( 𝜑 → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 rrhf.d 𝐷 = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
2 rrhf.j 𝐽 = ( topGen ‘ ran (,) )
3 rrhf.b 𝐵 = ( Base ‘ 𝑅 )
4 rrhf.k 𝐾 = ( TopOpen ‘ 𝑅 )
5 rrhf.z 𝑍 = ( ℤMod ‘ 𝑅 )
6 rrhf.1 ( 𝜑𝑅 ∈ DivRing )
7 rrhf.2 ( 𝜑𝑅 ∈ NrmRing )
8 rrhf.3 ( 𝜑𝑍 ∈ NrmMod )
9 rrhf.4 ( 𝜑 → ( chr ‘ 𝑅 ) = 0 )
10 rrhf.5 ( 𝜑𝑅 ∈ CUnifSp )
11 rrhf.6 ( 𝜑 → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ 𝐷 ) )
12 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
13 1 12 3 4 5 6 7 8 9 10 11 rrhcn ( 𝜑 → ( ℝHom ‘ 𝑅 ) ∈ ( ( topGen ‘ ran (,) ) Cn 𝐾 ) )
14 uniretop ℝ = ( topGen ‘ ran (,) )
15 eqid 𝐾 = 𝐾
16 14 15 cnf ( ( ℝHom ‘ 𝑅 ) ∈ ( ( topGen ‘ ran (,) ) Cn 𝐾 ) → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐾 )
17 13 16 syl ( 𝜑 → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐾 )
18 nrgngp ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
19 ngpxms ( 𝑅 ∈ NrmGrp → 𝑅 ∈ ∞MetSp )
20 7 18 19 3syl ( 𝜑𝑅 ∈ ∞MetSp )
21 xmstps ( 𝑅 ∈ ∞MetSp → 𝑅 ∈ TopSp )
22 3 4 tpsuni ( 𝑅 ∈ TopSp → 𝐵 = 𝐾 )
23 20 21 22 3syl ( 𝜑𝐵 = 𝐾 )
24 23 feq3d ( 𝜑 → ( ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐵 ↔ ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐾 ) )
25 17 24 mpbird ( 𝜑 → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐵 )