Metamath Proof Explorer


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 𝐵 = ( Base ‘ 𝑅 )
Assertion rrhfe ( 𝑅 ∈ ℝExt → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 rrhfe.b 𝐵 = ( Base ‘ 𝑅 )
2 eqid ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
3 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
4 eqid ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
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 1 2 rrextust ( 𝑅 ∈ ℝExt → ( UnifSt ‘ 𝑅 ) = ( metUnif ‘ ( ( dist ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) ) ) )
12 2 3 1 4 5 6 7 8 9 10 11 rrhf ( 𝑅 ∈ ℝExt → ( ℝHom ‘ 𝑅 ) : ℝ ⟶ 𝐵 )