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 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
xrge0iifhmeo.k ⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
Assertion xrge0iifmhm 𝐹 ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) MndHom ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
2 xrge0iifhmeo.k ⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
3 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) )
4 3 iistmd ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ TopMnd
5 tmdmnd ⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ TopMnd → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ Mnd )
6 4 5 ax-mp ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ Mnd
7 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
8 cmnmnd ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
9 7 8 ax-mp ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
10 6 9 pm3.2i ⊢ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ Mnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
11 1 xrge0iifcnv ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) ∧ ◡ 𝐹 = ( 𝑦 ∈ ( 0 [,] +∞ ) ↦ if ( 𝑦 = +∞ , 0 , ( exp ‘ - 𝑦 ) ) ) )
12 11 simpli ⊢ 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ )
13 f1of ⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 0 [,] +∞ ) → 𝐹 : ( 0 [,] 1 ) ⟶ ( 0 [,] +∞ ) )
14 12 13 ax-mp ⊢ 𝐹 : ( 0 [,] 1 ) ⟶ ( 0 [,] +∞ )
15 1 2 xrge0iifhom ⊢ ( ( 𝑦 ∈ ( 0 [,] 1 ) ∧ 𝑧 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) +𝑒 ( 𝐹 ‘ 𝑧 ) ) )
16 15 rgen2 ⊢ ∀ 𝑦 ∈ ( 0 [,] 1 ) ∀ 𝑧 ∈ ( 0 [,] 1 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) +𝑒 ( 𝐹 ‘ 𝑧 ) )
17 1 2 xrge0iif1 ⊢ ( 𝐹 ‘ 1 ) = 0
18 14 16 17 3pm3.2i ⊢ ( 𝐹 : ( 0 [,] 1 ) ⟶ ( 0 [,] +∞ ) ∧ ∀ 𝑦 ∈ ( 0 [,] 1 ) ∀ 𝑧 ∈ ( 0 [,] 1 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) +𝑒 ( 𝐹 ‘ 𝑧 ) ) ∧ ( 𝐹 ‘ 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 ) ↾s ( 0 [,] 1 ) ) ) )
24 19 23 ax-mp ⊢ ( 0 [,] 1 ) = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) )
25 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
26 cnfldex ⊢ ℂfld ∈ V
27 ovex ⊢ ( 0 [,] 1 ) ∈ V
28 eqid ⊢ ( ℂfld ↾s ( 0 [,] 1 ) ) = ( ℂfld ↾s ( 0 [,] 1 ) )
29 28 20 mgpress ⊢ ( ( ℂfld ∈ V ∧ ( 0 [,] 1 ) ∈ V ) → ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) ) )
30 26 27 29 mp2an ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) = ( mulGrp ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) )
31 cnfldmul ⊢ · = ( .r ‘ ℂfld )
32 28 31 ressmulr ⊢ ( ( 0 [,] 1 ) ∈ V → · = ( .r ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) ) )
33 27 32 ax-mp ⊢ · = ( .r ‘ ( ℂfld ↾s ( 0 [,] 1 ) ) )
34 30 33 mgpplusg ⊢ · = ( +g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) )
35 xrge0plusg ⊢ +𝑒 = ( +g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
36 cnring ⊢ ℂfld ∈ Ring
37 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
38 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
39 3 21 38 ringidss ⊢ ( ( ℂfld ∈ Ring ∧ ( 0 [,] 1 ) ⊆ ℂ ∧ 1 ∈ ( 0 [,] 1 ) ) → 1 = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ) )
40 36 19 37 39 mp3an ⊢ 1 = ( 0g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) )
41 xrge00 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
42 24 25 34 35 40 41 ismhm ⊢ ( 𝐹 ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) MndHom ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) ↔ ( ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) ∈ Mnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ) ∧ ( 𝐹 : ( 0 [,] 1 ) ⟶ ( 0 [,] +∞ ) ∧ ∀ 𝑦 ∈ ( 0 [,] 1 ) ∀ 𝑧 ∈ ( 0 [,] 1 ) ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) +𝑒 ( 𝐹 ‘ 𝑧 ) ) ∧ ( 𝐹 ‘ 1 ) = 0 ) ) )
43 10 18 42 mpbir2an ⊢ 𝐹 ∈ ( ( ( mulGrp ‘ ℂfld ) ↾s ( 0 [,] 1 ) ) MndHom ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )