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 ‘ 𝑅 ) : ℝ ⟶ 𝐵 )

Metamath Proof Explorer

Theorem rrhf

Proof