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 𝐽 = ( topGen ‘ ran (,) )
rrhcne.k 𝐾 = ( TopOpen ‘ 𝑅 )
Assertion rrhcne ( 𝑅 ∈ ℝExt → ( ℝHom ‘ 𝑅 ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 rrhcne.j 𝐽 = ( topGen ‘ ran (,) )
2 rrhcne.k 𝐾 = ( TopOpen ‘ 𝑅 )
3 eqid ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ( ℤMod ‘ 𝑅 ) = ( ℤMod ‘ 𝑅 )
6 rrextdrg ( 𝑅 ∈ ℝExt → 𝑅 ∈ DivRing )
7 rrextnrg ( 𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing )
8 5 rrextnlm ( 𝑅 ∈ ℝExt → ( ℤMod ‘ 𝑅 ) ∈ NrmMod )
9 rrextchr ( 𝑅 ∈ ℝExt → ( chr ‘ 𝑅 ) = 0 )
10 rrextcusp ( 𝑅 ∈ ℝExt → 𝑅 ∈ CUnifSp )
11 4 3 rrextust ( 𝑅 ∈ ℝExt → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) )
12 3 1 4 2 5 6 7 8 9 10 11 rrhcn ( 𝑅 ∈ ℝExt → ( ℝHom ‘ 𝑅 ) ∈ ( 𝐽 Cn 𝐾 ) )