Metamath Proof Explorer


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 )