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 ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ TopMnd

Proof

Step Hyp Ref Expression
1 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = 0 ↔ 𝑦 = 0 ) )
2 fveq2 ( 𝑥 = 𝑦 → ( log ‘ 𝑥 ) = ( log ‘ 𝑦 ) )
3 2 negeqd ( 𝑥 = 𝑦 → - ( log ‘ 𝑥 ) = - ( log ‘ 𝑦 ) )
4 1 3 ifbieq2d ( 𝑥 = 𝑦 → if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) = if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) )
5 4 cbvmptv ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) = ( 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) )
6 xrge0topn ( TopOpen ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
7 5 6 xrge0iifmhm ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) MndHom ( ℝ*𝑠s ( 0 [,] +∞ ) ) )
8 5 6 xrge0iifhmeo ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ∈ ( II Homeo ( TopOpen ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) ) )
9 cnfldex fld ∈ V
10 ovex ( 0 [,] 1 ) ∈ V
11 eqid ( ℂflds ( 0 [,] 1 ) ) = ( ℂflds ( 0 [,] 1 ) )
12 eqid ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
13 11 12 mgpress ( ( ℂfld ∈ V ∧ ( 0 [,] 1 ) ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂflds ( 0 [,] 1 ) ) ) )
14 9 10 13 mp2an ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂflds ( 0 [,] 1 ) ) )
15 11 dfii4 II = ( TopOpen ‘ ( ℂflds ( 0 [,] 1 ) ) )
16 14 15 mgptopn II = ( TopOpen ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) )
17 16 oveq1i ( II Homeo ( TopOpen ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) ) ) = ( ( TopOpen ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ) Homeo ( TopOpen ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) ) )
18 8 17 eleqtri ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) ) ∈ ( ( TopOpen ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ) Homeo ( TopOpen ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) ) )
19 eqid ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) )
20 19 iistmd ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ TopMnd
21 xrge0tps ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ TopSp
22 7 18 20 21 mhmhmeotmd ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ TopMnd