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 X. B ) )
	rrhf.j	|- J = ( topGen ` ran (,) )
	rrhf.b	|- B = ( Base ` R )
	rrhf.k	|- K = ( TopOpen ` R )
	rrhf.z	|- Z = ( ZMod ` R )
	rrhf.1	|- ( ph -> R e. DivRing )
	rrhf.2	|- ( ph -> R e. NrmRing )
	rrhf.3	|- ( ph -> Z e. NrmMod )
	rrhf.4	|- ( ph -> ( chr ` R ) = 0 )
	rrhf.5	|- ( ph -> R e. CUnifSp )
	rrhf.6	|- ( ph -> ( UnifSt ` R ) = ( metUnif ` D ) )
Assertion	rrhf	|- ( ph -> ( RRHom ` R ) : RR --> B )

Proof

Step	Hyp	Ref	Expression
1		rrhf.d	|- D = ( ( dist ` R ) |` ( B X. B ) )
2		rrhf.j	|- J = ( topGen ` ran (,) )
3		rrhf.b	|- B = ( Base ` R )
4		rrhf.k	|- K = ( TopOpen ` R )
5		rrhf.z	|- Z = ( ZMod ` R )
6		rrhf.1	|- ( ph -> R e. DivRing )
7		rrhf.2	|- ( ph -> R e. NrmRing )
8		rrhf.3	|- ( ph -> Z e. NrmMod )
9		rrhf.4	|- ( ph -> ( chr ` R ) = 0 )
10		rrhf.5	|- ( ph -> R e. CUnifSp )
11		rrhf.6	|- ( ph -> ( UnifSt ` R ) = ( metUnif ` D ) )
12		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
13	1 12 3 4 5 6 7 8 9 10 11	rrhcn	|- ( ph -> ( RRHom ` R ) e. ( ( topGen ` ran (,) ) Cn K ) )
14		uniretop	|- RR = U. ( topGen ` ran (,) )
15		eqid	|- U. K = U. K
16	14 15	cnf	|- ( ( RRHom ` R ) e. ( ( topGen ` ran (,) ) Cn K ) -> ( RRHom ` R ) : RR --> U. K )
17	13 16	syl	|- ( ph -> ( RRHom ` R ) : RR --> U. K )
18		nrgngp	|- ( R e. NrmRing -> R e. NrmGrp )
19		ngpxms	|- ( R e. NrmGrp -> R e. *MetSp )
20	7 18 19	3syl	|- ( ph -> R e. *MetSp )
21		xmstps	|- ( R e. *MetSp -> R e. TopSp )
22	3 4	tpsuni	|- ( R e. TopSp -> B = U. K )
23	20 21 22	3syl	|- ( ph -> B = U. K )
24	23	feq3d	|- ( ph -> ( ( RRHom ` R ) : RR --> B <-> ( RRHom ` R ) : RR --> U. K ) )
25	17 24	mpbird	|- ( ph -> ( RRHom ` R ) : RR --> B )