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 )