Step |
Hyp |
Ref |
Expression |
1 |
|
circgrp.1 |
|- C = ( `' abs " { 1 } ) |
2 |
|
circgrp.2 |
|- T = ( ( mulGrp ` CCfld ) |`s C ) |
3 |
|
oveq2 |
|- ( x = y -> ( _i x. x ) = ( _i x. y ) ) |
4 |
3
|
fveq2d |
|- ( x = y -> ( exp ` ( _i x. x ) ) = ( exp ` ( _i x. y ) ) ) |
5 |
4
|
cbvmptv |
|- ( x e. RR |-> ( exp ` ( _i x. x ) ) ) = ( y e. RR |-> ( exp ` ( _i x. y ) ) ) |
6 |
5 1
|
efifo |
|- ( x e. RR |-> ( exp ` ( _i x. x ) ) ) : RR -onto-> C |
7 |
|
forn |
|- ( ( x e. RR |-> ( exp ` ( _i x. x ) ) ) : RR -onto-> C -> ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) = C ) |
8 |
6 7
|
ax-mp |
|- ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) = C |
9 |
8
|
eqcomi |
|- C = ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) |
10 |
9
|
oveq2i |
|- ( ( mulGrp ` CCfld ) |`s C ) = ( ( mulGrp ` CCfld ) |`s ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) ) |
11 |
2 10
|
eqtri |
|- T = ( ( mulGrp ` CCfld ) |`s ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) ) |
12 |
|
ax-icn |
|- _i e. CC |
13 |
12
|
a1i |
|- ( T. -> _i e. CC ) |
14 |
|
resubdrg |
|- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing ) |
15 |
14
|
simpli |
|- RR e. ( SubRing ` CCfld ) |
16 |
|
subrgsubg |
|- ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) ) |
17 |
15 16
|
ax-mp |
|- RR e. ( SubGrp ` CCfld ) |
18 |
17
|
a1i |
|- ( T. -> RR e. ( SubGrp ` CCfld ) ) |
19 |
5 11 13 18
|
efabl |
|- ( T. -> T e. Abel ) |
20 |
19
|
mptru |
|- T e. Abel |