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 ) |