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={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}$$
	rrhf.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	rrhf.b	$$⊢B={\mathrm{Base}}_R$$
	rrhf.k	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
	rrhf.z	$$⊢Z=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
	rrhf.1	$$⊢\phi \to R\in \mathrm{DivRing}$$
	rrhf.2	$$⊢\phi \to R\in \mathrm{NrmRing}$$
	rrhf.3	$$⊢\phi \to Z\in \mathrm{NrmMod}$$
	rrhf.4	$$⊢\phi \to \mathrm{chr}\left(R\right)=0$$
	rrhf.5	$$⊢\phi \to R\in \mathrm{CUnifSp}$$
	rrhf.6	$$⊢\phi \to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)$$
Assertion	rrhf	$$⊢\phi \to \mathrm{ℝHom}\left(R\right):ℝ⟶B$$

Proof

Step	Hyp	Ref	Expression
1		rrhf.d	$$⊢D={\mathrm{dist}\left(R\right)\upharpoonright }_{\left(B\times B\right)}$$
2		rrhf.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		rrhf.b	$$⊢B={\mathrm{Base}}_R$$
4		rrhf.k	$$⊢K=\mathrm{TopOpen}\left(R\right)$$
5		rrhf.z	$$⊢Z=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
6		rrhf.1	$$⊢\phi \to R\in \mathrm{DivRing}$$
7		rrhf.2	$$⊢\phi \to R\in \mathrm{NrmRing}$$
8		rrhf.3	$$⊢\phi \to Z\in \mathrm{NrmMod}$$
9		rrhf.4	$$⊢\phi \to \mathrm{chr}\left(R\right)=0$$
10		rrhf.5	$$⊢\phi \to R\in \mathrm{CUnifSp}$$
11		rrhf.6	$$⊢\phi \to \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left(D\right)$$
12		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
13	1 12 3 4 5 6 7 8 9 10 11	rrhcn	$$⊢\phi \to \mathrm{ℝHom}\left(R\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}K\right)$$
14		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
15		eqid	$$⊢\bigcup K=\bigcup K$$
16	14 15	cnf	$$⊢\mathrm{ℝHom}\left(R\right)\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}K\right)\to \mathrm{ℝHom}\left(R\right):ℝ⟶\bigcup K$$
17	13 16	syl	$$⊢\phi \to \mathrm{ℝHom}\left(R\right):ℝ⟶\bigcup K$$
18		nrgngp	$$⊢R\in \mathrm{NrmRing}\to R\in \mathrm{NrmGrp}$$
19		ngpxms	$$⊢R\in \mathrm{NrmGrp}\to R\in \mathrm{\infty MetSp}$$
20	7 18 19	3syl	$$⊢\phi \to R\in \mathrm{\infty MetSp}$$
21		xmstps	$$⊢R\in \mathrm{\infty MetSp}\to R\in \mathrm{TopSp}$$
22	3 4	tpsuni	$$⊢R\in \mathrm{TopSp}\to B=\bigcup K$$
23	20 21 22	3syl	$$⊢\phi \to B=\bigcup K$$
24	23	feq3d	$$⊢\phi \to \left(\mathrm{ℝHom}\left(R\right):ℝ⟶B\leftrightarrow \mathrm{ℝHom}\left(R\right):ℝ⟶\bigcup K\right)$$
25	17 24	mpbird	$$⊢\phi \to \mathrm{ℝHom}\left(R\right):ℝ⟶B$$