Theorem rrhfe

Description: If R is an extension of RR , then the canonical homomorphism of RR into R is a function. (Contributed by Thierry Arnoux, 2-May-2018)

	Ref	Expression
Hypothesis	rrhfe.b	|- B = ( Base ` R )
Assertion	rrhfe	|- ( R e. RRExt -> ( RRHom ` R ) : RR --> B )

Proof

Step	Hyp	Ref	Expression
1		rrhfe.b	|- B = ( Base ` R )
2		eqid	|- ( ( dist ` R ) |` ( B X. B ) ) = ( ( dist ` R ) |` ( B X. B ) )
3		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
4		eqid	|- ( TopOpen ` R ) = ( TopOpen ` R )
5		eqid	|- ( ZMod ` R ) = ( ZMod ` R )
6		rrextdrg	|- ( R e. RRExt -> R e. DivRing )
7		rrextnrg	|- ( R e. RRExt -> R e. NrmRing )
8	5	rrextnlm	|- ( R e. RRExt -> ( ZMod ` R ) e. NrmMod )
9		rrextchr	|- ( R e. RRExt -> ( chr ` R ) = 0 )
10		rrextcusp	|- ( R e. RRExt -> R e. CUnifSp )
11	1 2	rrextust	|- ( R e. RRExt -> ( UnifSt ` R ) = ( metUnif ` ( ( dist ` R ) |` ( B X. B ) ) ) )
12	2 3 1 4 5 6 7 8 9 10 11	rrhf	|- ( R e. RRExt -> ( RRHom ` R ) : RR --> B )