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