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	1 2 3	3syl	$⊢ R \in ℝExt \to R \in ∞MetSp$
5		xmstps	$⊢ R \in ∞MetSp \to R \in TopSp$
6	4 5	syl	$⊢ R \in ℝExt \to R \in TopSp$