Metamath Proof Explorer

Theorem xrge0tmd

Description: The extended nonnegative real numbers monoid is a topological monoid. (Contributed by Thierry Arnoux, 26-Mar-2017) (Proof Shortened by Thierry Arnoux, 21-Jun-2017.)

Ref Expression
Assertion xrge0tmd 
|- ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = y -> ( x = 0 <-> y = 0 ) )
2 fveq2 
 |-  ( x = y -> ( log ` x ) = ( log ` y ) )
3 2 negeqd 
 |-  ( x = y -> -u ( log ` x ) = -u ( log ` y ) )
4 1 3 ifbieq2d 
 |-  ( x = y -> if ( x = 0 , +oo , -u ( log ` x ) ) = if ( y = 0 , +oo , -u ( log ` y ) ) )
5 4 cbvmptv 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) ) = ( y e. ( 0 [,] 1 ) |-> if ( y = 0 , +oo , -u ( log ` y ) ) )
6 xrge0topn 
 |-  ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
7 5 6 xrge0iifmhm 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) ) e. ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) MndHom ( RR*s |`s ( 0 [,] +oo ) ) )
8 5 6 xrge0iifhmeo 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) ) e. ( II Homeo ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
9 cnfldex 
 |-  CCfld e. _V
10 ovex 
 |-  ( 0 [,] 1 ) e. _V
11 eqid 
 |-  ( CCfld |`s ( 0 [,] 1 ) ) = ( CCfld |`s ( 0 [,] 1 ) )
12 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
13 11 12 mgpress 
 |-  ( ( CCfld e. _V /\ ( 0 [,] 1 ) e. _V ) -> ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( mulGrp ` ( CCfld |`s ( 0 [,] 1 ) ) ) )
14 9 10 13 mp2an 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( mulGrp ` ( CCfld |`s ( 0 [,] 1 ) ) )
15 11 dfii4 
 |-  II = ( TopOpen ` ( CCfld |`s ( 0 [,] 1 ) ) )
16 14 15 mgptopn 
 |-  II = ( TopOpen ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) )
17 16 oveq1i 
 |-  ( II Homeo ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) ) = ( ( TopOpen ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) ) Homeo ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
18 8 17 eleqtri 
 |-  ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) ) e. ( ( TopOpen ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) ) Homeo ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
19 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) )
20 19 iistmd 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. TopMnd
21 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
22 7 18 20 21 mhmhmeotmd 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd