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 ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ 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 → − log ⁡ x = − log ⁡ y
4 1 3 ifbieq2d ⊢ x = y → if x = 0 +∞ − log ⁡ x = if y = 0 +∞ − log ⁡ y
5 4 cbvmptv ⊢ x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x = y ∈ 0 1 ⟼ if y = 0 +∞ − log ⁡ y
6 xrge0topn ⊢ TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
7 5 6 xrge0iifmhm ⊢ x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x ∈ mulGrp ℂ fld ↾ 𝑠 0 1 MndHom ℝ 𝑠 * ↾ 𝑠 0 +∞
8 5 6 xrge0iifhmeo ⊢ x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x ∈ II Homeo TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
9 cnfldex ⊢ ℂ fld ∈ V
10 ovex ⊢ 0 1 ∈ V
11 eqid ⊢ ℂ fld ↾ 𝑠 0 1 = ℂ fld ↾ 𝑠 0 1
12 eqid ⊢ mulGrp ℂ fld = mulGrp ℂ fld
13 11 12 mgpress ⊢ ℂ fld ∈ V ∧ 0 1 ∈ V → mulGrp ℂ fld ↾ 𝑠 0 1 = mulGrp ℂ fld ↾ 𝑠 0 1
14 9 10 13 mp2an ⊢ mulGrp ℂ fld ↾ 𝑠 0 1 = mulGrp ℂ fld ↾ 𝑠 0 1
15 11 dfii4 ⊢ II = TopOpen ⁡ ℂ fld ↾ 𝑠 0 1
16 14 15 mgptopn ⊢ II = TopOpen ⁡ mulGrp ℂ fld ↾ 𝑠 0 1
17 16 oveq1i ⊢ II Homeo TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ = TopOpen ⁡ mulGrp ℂ fld ↾ 𝑠 0 1 Homeo TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
18 8 17 eleqtri ⊢ x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x ∈ TopOpen ⁡ mulGrp ℂ fld ↾ 𝑠 0 1 Homeo TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
19 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 0 1 = mulGrp ℂ fld ↾ 𝑠 0 1
20 19 iistmd ⊢ mulGrp ℂ fld ↾ 𝑠 0 1 ∈ TopMnd
21 xrge0tps ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
22 7 18 20 21 mhmhmeotmd ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopMnd