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 e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
xrge0iifhmeo.k 
|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
Assertion xrge0iifmhm 
|- F e. ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) MndHom ( RR*s |`s ( 0 [,] +oo ) ) )

Proof

Step Hyp Ref Expression
1 xrge0iifhmeo.1 
 |-  F = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
2 xrge0iifhmeo.k 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
3 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) )
4 3 iistmd 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. TopMnd
5 tmdmnd 
 |-  ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. TopMnd -> ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. Mnd )
6 4 5 ax-mp 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. Mnd
7 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
8 cmnmnd 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
9 7 8 ax-mp 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
10 6 9 pm3.2i 
 |-  ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. Mnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
11 1 xrge0iifcnv 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) /\ `' F = ( y e. ( 0 [,] +oo ) |-> if ( y = +oo , 0 , ( exp ` -u y ) ) ) )
12 11 simpli 
 |-  F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo )
13 f1of 
 |-  ( F : ( 0 [,] 1 ) -1-1-onto-> ( 0 [,] +oo ) -> F : ( 0 [,] 1 ) --> ( 0 [,] +oo ) )
14 12 13 ax-mp 
 |-  F : ( 0 [,] 1 ) --> ( 0 [,] +oo )
15 1 2 xrge0iifhom 
 |-  ( ( y e. ( 0 [,] 1 ) /\ z e. ( 0 [,] 1 ) ) -> ( F ` ( y x. z ) ) = ( ( F ` y ) +e ( F ` z ) ) )
16 15 rgen2 
 |-  A. y e. ( 0 [,] 1 ) A. z e. ( 0 [,] 1 ) ( F ` ( y x. z ) ) = ( ( F ` y ) +e ( F ` z ) )
17 1 2 xrge0iif1 
 |-  ( F ` 1 ) = 0
18 14 16 17 3pm3.2i 
 |-  ( F : ( 0 [,] 1 ) --> ( 0 [,] +oo ) /\ A. y e. ( 0 [,] 1 ) A. z e. ( 0 [,] 1 ) ( F ` ( y x. z ) ) = ( ( F ` y ) +e ( F ` z ) ) /\ ( F ` 1 ) = 0 )
19 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
20 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
21 cnfldbas 
 |-  CC = ( Base ` CCfld )
22 20 21 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
23 3 22 ressbas2 
 |-  ( ( 0 [,] 1 ) C_ CC -> ( 0 [,] 1 ) = ( Base ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) ) )
24 19 23 ax-mp 
 |-  ( 0 [,] 1 ) = ( Base ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) )
25 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
26 cnfldex 
 |-  CCfld e. _V
27 ovex 
 |-  ( 0 [,] 1 ) e. _V
28 eqid 
 |-  ( CCfld |`s ( 0 [,] 1 ) ) = ( CCfld |`s ( 0 [,] 1 ) )
29 28 20 mgpress 
 |-  ( ( CCfld e. _V /\ ( 0 [,] 1 ) e. _V ) -> ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( mulGrp ` ( CCfld |`s ( 0 [,] 1 ) ) ) )
30 26 27 29 mp2an 
 |-  ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) = ( mulGrp ` ( CCfld |`s ( 0 [,] 1 ) ) )
31 cnfldmul 
 |-  x. = ( .r ` CCfld )
32 28 31 ressmulr 
 |-  ( ( 0 [,] 1 ) e. _V -> x. = ( .r ` ( CCfld |`s ( 0 [,] 1 ) ) ) )
33 27 32 ax-mp 
 |-  x. = ( .r ` ( CCfld |`s ( 0 [,] 1 ) ) )
34 30 33 mgpplusg 
 |-  x. = ( +g ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) )
35 xrge0plusg 
 |-  +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) )
36 cnring 
 |-  CCfld e. Ring
37 1elunit 
 |-  1 e. ( 0 [,] 1 )
38 cnfld1 
 |-  1 = ( 1r ` CCfld )
39 3 21 38 ringidss 
 |-  ( ( CCfld e. Ring /\ ( 0 [,] 1 ) C_ CC /\ 1 e. ( 0 [,] 1 ) ) -> 1 = ( 0g ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) ) )
40 36 19 37 39 mp3an 
 |-  1 = ( 0g ` ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) )
41 xrge00 
 |-  0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
42 24 25 34 35 40 41 ismhm 
 |-  ( F e. ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) MndHom ( RR*s |`s ( 0 [,] +oo ) ) ) <-> ( ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) e. Mnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd ) /\ ( F : ( 0 [,] 1 ) --> ( 0 [,] +oo ) /\ A. y e. ( 0 [,] 1 ) A. z e. ( 0 [,] 1 ) ( F ` ( y x. z ) ) = ( ( F ` y ) +e ( F ` z ) ) /\ ( F ` 1 ) = 0 ) ) )
43 10 18 42 mpbir2an 
 |-  F e. ( ( ( mulGrp ` CCfld ) |`s ( 0 [,] 1 ) ) MndHom ( RR*s |`s ( 0 [,] +oo ) ) )