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 ⊢ R ∈ ℝExt → R ∈ TopSp

Proof

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