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 \in ℝExt \to R \in TopSp$

Step	Hyp	Ref	Expression
1		rrextnrg	$⊢ R \in ℝExt \to R \in NrmRing$
2		nrgngp	$⊢ R \in NrmRing \to R \in NrmGrp$
3		ngpxms	$⊢ R \in NrmGrp \to R \in ∞MetSp$
4		xmstps	$⊢ R \in ∞MetSp \to R \in TopSp$
5	1 2 3 4	4syl	$⊢ R \in ℝExt \to R \in TopSp$