Metamath Proof Explorer


Theorem rrhcne

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

Ref Expression
Hypotheses rrhcne.j
|- J = ( topGen ` ran (,) )
rrhcne.k
|- K = ( TopOpen ` R )
Assertion rrhcne
|- ( R e. RRExt -> ( RRHom ` R ) e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 rrhcne.j
 |-  J = ( topGen ` ran (,) )
2 rrhcne.k
 |-  K = ( TopOpen ` R )
3 eqid
 |-  ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) )
4 eqid
 |-  ( Base ` R ) = ( Base ` 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 4 3 rrextust
 |-  ( R e. RRExt -> ( UnifSt ` R ) = ( metUnif ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) )
12 3 1 4 2 5 6 7 8 9 10 11 rrhcn
 |-  ( R e. RRExt -> ( RRHom ` R ) e. ( J Cn K ) )