# 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}=\left({x}\in \left[0,1\right]⟼if\left({x}=0,\mathrm{+\infty },-\mathrm{log}{x}\right)\right)$
xrge0iifhmeo.k ${⊢}{J}=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]$
Assertion xrge0iifmhm ${⊢}{F}\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)\mathrm{MndHom}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\right)$

### Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ${⊢}{F}=\left({x}\in \left[0,1\right]⟼if\left({x}=0,\mathrm{+\infty },-\mathrm{log}{x}\right)\right)$
2 xrge0iifhmeo.k ${⊢}{J}=\mathrm{ordTop}\left(\le \right){↾}_{𝑡}\left[0,\mathrm{+\infty }\right]$
3 eqid ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]$
4 3 iistmd ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\in \mathrm{TopMnd}$
5 tmdmnd ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\in \mathrm{TopMnd}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\in \mathrm{Mnd}$
6 4 5 ax-mp ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\in \mathrm{Mnd}$
7 xrge0cmn ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}$
8 cmnmnd ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{CMnd}\to {ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}$
9 7 8 ax-mp ${⊢}{ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}$
10 6 9 pm3.2i ${⊢}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\in \mathrm{Mnd}\wedge {ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}\right)$
11 1 xrge0iifcnv ${⊢}\left({F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right]\wedge {{F}}^{-1}=\left({y}\in \left[0,\mathrm{+\infty }\right]⟼if\left({y}=\mathrm{+\infty },0,{\mathrm{e}}^{-{y}}\right)\right)\right)$
12 11 simpli ${⊢}{F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right]$
13 f1of ${⊢}{F}:\left[0,1\right]\underset{1-1 onto}{⟶}\left[0,\mathrm{+\infty }\right]\to {F}:\left[0,1\right]⟶\left[0,\mathrm{+\infty }\right]$
14 12 13 ax-mp ${⊢}{F}:\left[0,1\right]⟶\left[0,\mathrm{+\infty }\right]$
15 1 2 xrge0iifhom ${⊢}\left({y}\in \left[0,1\right]\wedge {z}\in \left[0,1\right]\right)\to {F}\left({y}{z}\right)={F}\left({y}\right){+}_{𝑒}{F}\left({z}\right)$
16 15 rgen2 ${⊢}\forall {y}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{F}\left({y}{z}\right)={F}\left({y}\right){+}_{𝑒}{F}\left({z}\right)$
17 1 2 xrge0iif1 ${⊢}{F}\left(1\right)=0$
18 14 16 17 3pm3.2i ${⊢}\left({F}:\left[0,1\right]⟶\left[0,\mathrm{+\infty }\right]\wedge \forall {y}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{F}\left({y}{z}\right)={F}\left({y}\right){+}_{𝑒}{F}\left({z}\right)\wedge {F}\left(1\right)=0\right)$
19 unitsscn ${⊢}\left[0,1\right]\subseteq ℂ$
20 eqid ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$
21 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
22 20 21 mgpbas ${⊢}ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$
23 3 22 ressbas2 ${⊢}\left[0,1\right]\subseteq ℂ\to \left[0,1\right]={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)}$
24 19 23 ax-mp ${⊢}\left[0,1\right]={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)}$
25 xrge0base ${⊢}\left[0,\mathrm{+\infty }\right]={\mathrm{Base}}_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
26 cnfldex ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{V}$
27 ovex ${⊢}\left[0,1\right]\in \mathrm{V}$
28 eqid ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left[0,1\right]={ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left[0,1\right]$
29 28 20 mgpress ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{V}\wedge \left[0,1\right]\in \mathrm{V}\right)\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]={\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left[0,1\right]\right)}$
30 26 27 29 mp2an ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]={\mathrm{mulGrp}}_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left[0,1\right]\right)}$
31 cnfldmul ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
32 28 31 ressmulr ${⊢}\left[0,1\right]\in \mathrm{V}\to ×={\cdot }_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left[0,1\right]\right)}$
33 27 32 ax-mp ${⊢}×={\cdot }_{\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}\left[0,1\right]\right)}$
34 30 33 mgpplusg ${⊢}×={+}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)}$
35 xrge0plusg ${⊢}{+}_{𝑒}={+}_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
36 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
37 1elunit ${⊢}1\in \left[0,1\right]$
38 cnfld1 ${⊢}1={1}_{{ℂ}_{\mathrm{fld}}}$
39 3 21 38 ringidss ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\wedge \left[0,1\right]\subseteq ℂ\wedge 1\in \left[0,1\right]\right)\to 1={0}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)}$
40 36 19 37 39 mp3an ${⊢}1={0}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)}$
41 xrge00 ${⊢}0={0}_{\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)}$
42 24 25 34 35 40 41 ismhm ${⊢}{F}\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)\mathrm{MndHom}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\right)↔\left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\in \mathrm{Mnd}\wedge {ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\in \mathrm{Mnd}\right)\wedge \left({F}:\left[0,1\right]⟶\left[0,\mathrm{+\infty }\right]\wedge \forall {y}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {z}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}{F}\left({y}{z}\right)={F}\left({y}\right){+}_{𝑒}{F}\left({z}\right)\wedge {F}\left(1\right)=0\right)\right)$
43 10 18 42 mpbir2an ${⊢}{F}\in \left(\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{↾}_{𝑠}\left[0,1\right]\right)\mathrm{MndHom}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\right)$