Metamath Proof Explorer

Theorem xrge0iifmhm

Description: The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017)

Ref Expression
Hypotheses xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=0+∞−log⁡x
xrge0iifhmeo.k ⊢J=ordTop⁡≤↾𝑡0+∞
Assertion xrge0iifmhm ⊢F∈mulGrpℂfld↾𝑠01MndHomℝ𝑠*↾𝑠0+∞

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢F=x∈01⟼ifx=0+∞−log⁡x
2 xrge0iifhmeo.k ⊢J=ordTop⁡≤↾𝑡0+∞
3 eqid ⊢mulGrpℂfld↾𝑠01=mulGrpℂfld↾𝑠01
4 3 iistmd ⊢mulGrpℂfld↾𝑠01∈TopMnd
5 tmdmnd ⊢mulGrpℂfld↾𝑠01∈TopMnd→mulGrpℂfld↾𝑠01∈Mnd
6 4 5 ax-mp ⊢mulGrpℂfld↾𝑠01∈Mnd
7 xrge0cmn ⊢ℝ𝑠*↾𝑠0+∞∈CMnd
8 cmnmnd ⊢ℝ𝑠*↾𝑠0+∞∈CMnd→ℝ𝑠*↾𝑠0+∞∈Mnd
9 7 8 ax-mp ⊢ℝ𝑠*↾𝑠0+∞∈Mnd
10 6 9 pm3.2i ⊢mulGrpℂfld↾𝑠01∈Mnd∧ℝ𝑠*↾𝑠0+∞∈Mnd
11 1 xrge0iifcnv ⊢F:01⟶1-1 onto0+∞∧F-1=y∈0+∞⟼ify=+∞0e−y
12 11 simpli ⊢F:01⟶1-1 onto0+∞
13 f1of ⊢F:01⟶1-1 onto0+∞→F:01⟶0+∞
14 12 13 ax-mp ⊢F:01⟶0+∞
15 1 2 xrge0iifhom ⊢y∈01∧z∈01→F⁡y⁢z=F⁡y+𝑒F⁡z
16 15 rgen2 ⊢∀y∈01∀z∈01F⁡y⁢z=F⁡y+𝑒F⁡z
17 1 2 xrge0iif1 ⊢F⁡1=0
18 14 16 17 3pm3.2i ⊢F:01⟶0+∞∧∀y∈01∀z∈01F⁡y⁢z=F⁡y+𝑒F⁡z∧F⁡1=0
19 unitsscn ⊢01⊆ℂ
20 eqid ⊢mulGrpℂfld=mulGrpℂfld
21 cnfldbas ⊢ℂ=Baseℂfld
22 20 21 mgpbas ⊢ℂ=BasemulGrpℂfld
23 3 22 ressbas2 ⊢01⊆ℂ→01=BasemulGrpℂfld↾𝑠01
24 19 23 ax-mp ⊢01=BasemulGrpℂfld↾𝑠01
25 xrge0base ⊢0+∞=Baseℝ𝑠*↾𝑠0+∞
26 cnfldex ⊢ℂfld∈V
27 ovex ⊢01∈V
28 eqid ⊢ℂfld↾𝑠01=ℂfld↾𝑠01
29 28 20 mgpress ⊢ℂfld∈V∧01∈V→mulGrpℂfld↾𝑠01=mulGrpℂfld↾𝑠01
30 26 27 29 mp2an ⊢mulGrpℂfld↾𝑠01=mulGrpℂfld↾𝑠01
31 cnfldmul ⊢×=⋅ℂfld
32 28 31 ressmulr ⊢01∈V→×=⋅ℂfld↾𝑠01
33 27 32 ax-mp ⊢×=⋅ℂfld↾𝑠01
34 30 33 mgpplusg ⊢×=+mulGrpℂfld↾𝑠01
35 xrge0plusg ⊢+𝑒=+ℝ𝑠*↾𝑠0+∞
36 cnring ⊢ℂfld∈Ring
37 1elunit ⊢1∈01
38 cnfld1 ⊢1=1ℂfld
39 3 21 38 ringidss ⊢ℂfld∈Ring∧01⊆ℂ∧1∈01→1=0mulGrpℂfld↾𝑠01
40 36 19 37 39 mp3an ⊢1=0mulGrpℂfld↾𝑠01
41 xrge00 ⊢0=0ℝ𝑠*↾𝑠0+∞
42 24 25 34 35 40 41 ismhm ⊢F∈mulGrpℂfld↾𝑠01MndHomℝ𝑠*↾𝑠0+∞↔mulGrpℂfld↾𝑠01∈Mnd∧ℝ𝑠*↾𝑠0+∞∈Mnd∧F:01⟶0+∞∧∀y∈01∀z∈01F⁡y⁢z=F⁡y+𝑒F⁡z∧F⁡1=0
43 10 18 42 mpbir2an ⊢F∈mulGrpℂfld↾𝑠01MndHomℝ𝑠*↾𝑠0+∞