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 
|- K = ( TopOpen ` R )
Assertion rrexthaus 
|- ( R e. RRExt -> K e. Haus )

Proof

Step Hyp Ref Expression
1 rrexthaus.1 
 |-  K = ( TopOpen ` R )
2 rrextnrg 
 |-  ( R e. RRExt -> R e. NrmRing )
3 nrgngp 
 |-  ( R e. NrmRing -> R e. NrmGrp )
4 ngpxms 
 |-  ( R e. NrmGrp -> R e. *MetSp )
5 2 3 4 3syl 
 |-  ( R e. RRExt -> R e. *MetSp )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) )
8 1 6 7 xmstopn 
 |-  ( R e. *MetSp -> K = ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) )
9 5 8 syl 
 |-  ( R e. RRExt -> K = ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) )
10 6 7 xmsxmet 
 |-  ( R e. *MetSp -> ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) e. ( *Met ` ( Base ` R ) ) )
11 eqid 
 |-  ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) = ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) )
12 11 methaus 
 |-  ( ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) e. ( *Met ` ( Base ` R ) ) -> ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) e. Haus )
13 5 10 12 3syl 
 |-  ( R e. RRExt -> ( MetOpen ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) e. Haus )
14 9 13 eqeltrd 
 |-  ( R e. RRExt -> K e. Haus )