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 ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
xrge0iifhmeo.k ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
Assertion xrge0iifmhm ⊢ F ∈ mulGrp ℂ fld ↾ 𝑠 0 1 MndHom ℝ 𝑠 * ↾ 𝑠 0 +∞

Proof

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