Theorem rrexthaus

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

	Ref	Expression
Hypothesis	rrexthaus.1	⊢ 𝐾 = ( TopOpen ‘ 𝑅 )
Assertion	rrexthaus	⊢ ( 𝑅 ∈ ℝExt → 𝐾 ∈ Haus )

Proof

Step	Hyp	Ref	Expression
1		rrexthaus.1	⊢ 𝐾 = ( TopOpen ‘ 𝑅 )
2		rrextnrg	⊢ ( 𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing )
3		nrgngp	⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
4		ngpxms	⊢ ( 𝑅 ∈ NrmGrp → 𝑅 ∈ ∞MetSp )
5	2 3 4	3syl	⊢ ( 𝑅 ∈ ℝExt → 𝑅 ∈ ∞MetSp )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7		eqid	⊢ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
8	1 6 7	xmstopn	⊢ ( 𝑅 ∈ ∞MetSp → 𝐾 = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) )
9	5 8	syl	⊢ ( 𝑅 ∈ ℝExt → 𝐾 = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) )
10	6 7	xmsxmet	⊢ ( 𝑅 ∈ ∞MetSp → ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑅 ) ) )
11		eqid	⊢ ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) )
12	11	methaus	⊢ ( ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑅 ) ) → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) ∈ Haus )
13	5 10 12	3syl	⊢ ( 𝑅 ∈ ℝExt → ( MetOpen ‘ ( ( dist ‘ 𝑅 ) ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) ) ∈ Haus )
14	9 13	eqeltrd	⊢ ( 𝑅 ∈ ℝExt → 𝐾 ∈ Haus )