rrexthaus

Description: The topology of an extension of RR is Hausdorff. (Contributed by Thierry Arnoux, 7-Sep-2018)

		Ref	Expression
	Hypothesis	rrexthaus.1	$⊢ K = TopOpen (R)$
	Assertion	rrexthaus	$⊢ R \in ℝExt \to K \in Haus$

Step	Hyp	Ref	Expression
1		rrexthaus.1	$⊢ K = TopOpen (R)$
2		rrextnrg	$⊢ R \in ℝExt \to R \in NrmRing$
3		nrgngp	$⊢ R \in NrmRing \to R \in NrmGrp$
4		ngpxms	$⊢ R \in NrmGrp \to R \in ∞MetSp$
5	2 3 4	3syl	$⊢ R \in ℝExt \to R \in ∞MetSp$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} = {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}$
8	1 6 7	xmstopn	$⊢ R \in ∞MetSp \to K = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
9	5 8	syl	$⊢ R \in ℝExt \to K = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
10	6 7	xmsxmet	$⊢ R \in ∞MetSp \to {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} \in ∞Met ({Base}_{R})$
11		eqid	$⊢ MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) = MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})$
12	11	methaus	$⊢ {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} \in ∞Met ({Base}_{R}) \to MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) \in Haus$
13	5 10 12	3syl	$⊢ R \in ℝExt \to MetOpen ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}) \in Haus$
14	9 13	eqeltrd	$⊢ R \in ℝExt \to K \in Haus$

Metamath Proof Explorer