Metamath Proof Explorer


Theorem rrexttps

Description: An extension of RR is a topological space. (Contributed by Thierry Arnoux, 7-Sep-2018)

Ref Expression
Assertion rrexttps ( 𝑅 ∈ ℝExt → 𝑅 ∈ TopSp )

Proof

Step Hyp Ref Expression
1 rrextnrg ( 𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing )
2 nrgngp ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
3 ngpxms ( 𝑅 ∈ NrmGrp → 𝑅 ∈ ∞MetSp )
4 1 2 3 3syl ( 𝑅 ∈ ℝExt → 𝑅 ∈ ∞MetSp )
5 xmstps ( 𝑅 ∈ ∞MetSp → 𝑅 ∈ TopSp )
6 4 5 syl ( 𝑅 ∈ ℝExt → 𝑅 ∈ TopSp )