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 ⊢ ( ℂfld ↾s ( 0 [,] 1 ) ) = ( ℂfld ↾s ( 0 [,] 1 ) )
12 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
13 11 12 mgpress ⊢ ( ( ℂfld ∈ V ∧ ( 0 [,] 1 ) ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) ) )
14 9 10 13 mp2an ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) )
15 11 dfii4 ⊢ II = ( TopOpen ‘ ( ℂfld ↾s ( 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