Metamath Proof Explorer

Theorem reefgim

Description: The exponential function is a group isomorphism from the group of reals under addition to the group of positive reals under multiplication. (Contributed by Mario Carneiro, 21-Jun-2015) (Revised by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypothesis reefgim.1 
|- P = ( ( mulGrp ` CCfld ) |`s RR+ )
Assertion reefgim 
|- ( exp |` RR ) e. ( RRfld GrpIso P )

Proof

Step Hyp Ref Expression
1 reefgim.1 
 |-  P = ( ( mulGrp ` CCfld ) |`s RR+ )
2 rebase 
 |-  RR = ( Base ` RRfld )
3 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
4 3 rpmsubg 
 |-  RR+ e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
5 cnex 
 |-  CC e. _V
6 5 difexi 
 |-  ( CC \ { 0 } ) e. _V
7 rpcndif0 
 |-  ( x e. RR+ -> x e. ( CC \ { 0 } ) )
8 7 ssriv 
 |-  RR+ C_ ( CC \ { 0 } )
9 ressabs 
 |-  ( ( ( CC \ { 0 } ) e. _V /\ RR+ C_ ( CC \ { 0 } ) ) -> ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s RR+ ) = ( ( mulGrp ` CCfld ) |`s RR+ ) )
10 6 8 9 mp2an 
 |-  ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s RR+ ) = ( ( mulGrp ` CCfld ) |`s RR+ )
11 1 10 eqtr4i 
 |-  P = ( ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |`s RR+ )
12 11 subgbas 
 |-  ( RR+ e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) -> RR+ = ( Base ` P ) )
13 4 12 ax-mp 
 |-  RR+ = ( Base ` P )
14 replusg 
 |-  + = ( +g ` RRfld )
15 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
16 cnfldmul 
 |-  x. = ( .r ` CCfld )
17 15 16 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
18 1 17 ressplusg 
 |-  ( RR+ e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) -> x. = ( +g ` P ) )
19 4 18 ax-mp 
 |-  x. = ( +g ` P )
20 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
21 20 simpli 
 |-  RR e. ( SubRing ` CCfld )
22 df-refld 
 |-  RRfld = ( CCfld |`s RR )
23 22 subrgring 
 |-  ( RR e. ( SubRing ` CCfld ) -> RRfld e. Ring )
24 21 23 ax-mp 
 |-  RRfld e. Ring
25 ringgrp 
 |-  ( RRfld e. Ring -> RRfld e. Grp )
26 24 25 mp1i 
 |-  ( T. -> RRfld e. Grp )
27 11 subggrp 
 |-  ( RR+ e. ( SubGrp ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) -> P e. Grp )
28 4 27 mp1i 
 |-  ( T. -> P e. Grp )
29 reeff1o 
 |-  ( exp |` RR ) : RR -1-1-onto-> RR+
30 f1of 
 |-  ( ( exp |` RR ) : RR -1-1-onto-> RR+ -> ( exp |` RR ) : RR --> RR+ )
31 29 30 mp1i 
 |-  ( T. -> ( exp |` RR ) : RR --> RR+ )
32 recn 
 |-  ( x e. RR -> x e. CC )
33 recn 
 |-  ( y e. RR -> y e. CC )
34 efadd 
 |-  ( ( x e. CC /\ y e. CC ) -> ( exp ` ( x + y ) ) = ( ( exp ` x ) x. ( exp ` y ) ) )
35 32 33 34 syl2an 
 |-  ( ( x e. RR /\ y e. RR ) -> ( exp ` ( x + y ) ) = ( ( exp ` x ) x. ( exp ` y ) ) )
36 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
37 36 fvresd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( exp |` RR ) ` ( x + y ) ) = ( exp ` ( x + y ) ) )
38 fvres 
 |-  ( x e. RR -> ( ( exp |` RR ) ` x ) = ( exp ` x ) )
39 fvres 
 |-  ( y e. RR -> ( ( exp |` RR ) ` y ) = ( exp ` y ) )
40 38 39 oveqan12d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( exp |` RR ) ` x ) x. ( ( exp |` RR ) ` y ) ) = ( ( exp ` x ) x. ( exp ` y ) ) )
41 35 37 40 3eqtr4d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( exp |` RR ) ` ( x + y ) ) = ( ( ( exp |` RR ) ` x ) x. ( ( exp |` RR ) ` y ) ) )
42 41 adantl 
 |-  ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( ( exp |` RR ) ` ( x + y ) ) = ( ( ( exp |` RR ) ` x ) x. ( ( exp |` RR ) ` y ) ) )
43 2 13 14 19 26 28 31 42 isghmd 
 |-  ( T. -> ( exp |` RR ) e. ( RRfld GrpHom P ) )
44 43 mptru 
 |-  ( exp |` RR ) e. ( RRfld GrpHom P )
45 2 13 isgim 
 |-  ( ( exp |` RR ) e. ( RRfld GrpIso P ) <-> ( ( exp |` RR ) e. ( RRfld GrpHom P ) /\ ( exp |` RR ) : RR -1-1-onto-> RR+ ) )
46 44 29 45 mpbir2an 
 |-  ( exp |` RR ) e. ( RRfld GrpIso P )