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 โŠข ๐‘ƒ = ( ( mulGrp โ€˜ โ„‚fld ) โ†พs โ„+ )
Assertion reefgim ( exp โ†พ โ„ ) โˆˆ ( โ„fld GrpIso ๐‘ƒ )

Proof

Step Hyp Ref Expression
1 reefgim.1 โŠข ๐‘ƒ = ( ( mulGrp โ€˜ โ„‚fld ) โ†พs โ„+ )
2 rebase โŠข โ„ = ( Base โ€˜ โ„fld )
3 eqid โŠข ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) = ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) )
4 3 rpmsubg โŠข โ„+ โˆˆ ( SubGrp โ€˜ ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) )
5 cnex โŠข โ„‚ โˆˆ V
6 5 difexi โŠข ( โ„‚ โˆ– { 0 } ) โˆˆ V
7 rpcndif0 โŠข ( ๐‘ฅ โˆˆ โ„+ โ†’ ๐‘ฅ โˆˆ ( โ„‚ โˆ– { 0 } ) )
8 7 ssriv โŠข โ„+ โŠ† ( โ„‚ โˆ– { 0 } )
9 ressabs โŠข ( ( ( โ„‚ โˆ– { 0 } ) โˆˆ V โˆง โ„+ โŠ† ( โ„‚ โˆ– { 0 } ) ) โ†’ ( ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) โ†พs โ„+ ) = ( ( mulGrp โ€˜ โ„‚fld ) โ†พs โ„+ ) )
10 6 8 9 mp2an โŠข ( ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) โ†พs โ„+ ) = ( ( mulGrp โ€˜ โ„‚fld ) โ†พs โ„+ )
11 1 10 eqtr4i โŠข ๐‘ƒ = ( ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) โ†พs โ„+ )
12 11 subgbas โŠข ( โ„+ โˆˆ ( SubGrp โ€˜ ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) ) โ†’ โ„+ = ( Base โ€˜ ๐‘ƒ ) )
13 4 12 ax-mp โŠข โ„+ = ( Base โ€˜ ๐‘ƒ )
14 replusg โŠข + = ( +g โ€˜ โ„fld )
15 eqid โŠข ( mulGrp โ€˜ โ„‚fld ) = ( mulGrp โ€˜ โ„‚fld )
16 cnfldmul โŠข ยท = ( .r โ€˜ โ„‚fld )
17 15 16 mgpplusg โŠข ยท = ( +g โ€˜ ( mulGrp โ€˜ โ„‚fld ) )
18 1 17 ressplusg โŠข ( โ„+ โˆˆ ( SubGrp โ€˜ ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) ) โ†’ ยท = ( +g โ€˜ ๐‘ƒ ) )
19 4 18 ax-mp โŠข ยท = ( +g โ€˜ ๐‘ƒ )
20 resubdrg โŠข ( โ„ โˆˆ ( SubRing โ€˜ โ„‚fld ) โˆง โ„fld โˆˆ DivRing )
21 20 simpli โŠข โ„ โˆˆ ( SubRing โ€˜ โ„‚fld )
22 df-refld โŠข โ„fld = ( โ„‚fld โ†พs โ„ )
23 22 subrgring โŠข ( โ„ โˆˆ ( SubRing โ€˜ โ„‚fld ) โ†’ โ„fld โˆˆ Ring )
24 21 23 ax-mp โŠข โ„fld โˆˆ Ring
25 ringgrp โŠข ( โ„fld โˆˆ Ring โ†’ โ„fld โˆˆ Grp )
26 24 25 mp1i โŠข ( โŠค โ†’ โ„fld โˆˆ Grp )
27 11 subggrp โŠข ( โ„+ โˆˆ ( SubGrp โ€˜ ( ( mulGrp โ€˜ โ„‚fld ) โ†พs ( โ„‚ โˆ– { 0 } ) ) ) โ†’ ๐‘ƒ โˆˆ Grp )
28 4 27 mp1i โŠข ( โŠค โ†’ ๐‘ƒ โˆˆ Grp )
29 reeff1o โŠข ( exp โ†พ โ„ ) : โ„ โ€“1-1-ontoโ†’ โ„+
30 f1of โŠข ( ( exp โ†พ โ„ ) : โ„ โ€“1-1-ontoโ†’ โ„+ โ†’ ( exp โ†พ โ„ ) : โ„ โŸถ โ„+ )
31 29 30 mp1i โŠข ( โŠค โ†’ ( exp โ†พ โ„ ) : โ„ โŸถ โ„+ )
32 recn โŠข ( ๐‘ฅ โˆˆ โ„ โ†’ ๐‘ฅ โˆˆ โ„‚ )
33 recn โŠข ( ๐‘ฆ โˆˆ โ„ โ†’ ๐‘ฆ โˆˆ โ„‚ )
34 efadd โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( exp โ€˜ ( ๐‘ฅ + ๐‘ฆ ) ) = ( ( exp โ€˜ ๐‘ฅ ) ยท ( exp โ€˜ ๐‘ฆ ) ) )
35 32 33 34 syl2an โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) โ†’ ( exp โ€˜ ( ๐‘ฅ + ๐‘ฆ ) ) = ( ( exp โ€˜ ๐‘ฅ ) ยท ( exp โ€˜ ๐‘ฆ ) ) )
36 readdcl โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) โ†’ ( ๐‘ฅ + ๐‘ฆ ) โˆˆ โ„ )
37 36 fvresd โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) โ†’ ( ( exp โ†พ โ„ ) โ€˜ ( ๐‘ฅ + ๐‘ฆ ) ) = ( exp โ€˜ ( ๐‘ฅ + ๐‘ฆ ) ) )
38 fvres โŠข ( ๐‘ฅ โˆˆ โ„ โ†’ ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฅ ) = ( exp โ€˜ ๐‘ฅ ) )
39 fvres โŠข ( ๐‘ฆ โˆˆ โ„ โ†’ ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฆ ) = ( exp โ€˜ ๐‘ฆ ) )
40 38 39 oveqan12d โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) โ†’ ( ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฅ ) ยท ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฆ ) ) = ( ( exp โ€˜ ๐‘ฅ ) ยท ( exp โ€˜ ๐‘ฆ ) ) )
41 35 37 40 3eqtr4d โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) โ†’ ( ( exp โ†พ โ„ ) โ€˜ ( ๐‘ฅ + ๐‘ฆ ) ) = ( ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฅ ) ยท ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฆ ) ) )
42 41 adantl โŠข ( ( โŠค โˆง ( ๐‘ฅ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ ) ) โ†’ ( ( exp โ†พ โ„ ) โ€˜ ( ๐‘ฅ + ๐‘ฆ ) ) = ( ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฅ ) ยท ( ( exp โ†พ โ„ ) โ€˜ ๐‘ฆ ) ) )
43 2 13 14 19 26 28 31 42 isghmd โŠข ( โŠค โ†’ ( exp โ†พ โ„ ) โˆˆ ( โ„fld GrpHom ๐‘ƒ ) )
44 43 mptru โŠข ( exp โ†พ โ„ ) โˆˆ ( โ„fld GrpHom ๐‘ƒ )
45 2 13 isgim โŠข ( ( exp โ†พ โ„ ) โˆˆ ( โ„fld GrpIso ๐‘ƒ ) โ†” ( ( exp โ†พ โ„ ) โˆˆ ( โ„fld GrpHom ๐‘ƒ ) โˆง ( exp โ†พ โ„ ) : โ„ โ€“1-1-ontoโ†’ โ„+ ) )
46 44 29 45 mpbir2an โŠข ( exp โ†พ โ„ ) โˆˆ ( โ„fld GrpIso ๐‘ƒ )