| 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 |
|
ax-icn |
|- _i e. CC |
| 12 |
11
|
a1i |
|- ( T. -> _i e. CC ) |
| 13 |
|
resubdrg |
|- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing ) |
| 14 |
13
|
simpli |
|- RR e. ( SubRing ` CCfld ) |
| 15 |
|
subrgsubg |
|- ( RR e. ( SubRing ` CCfld ) -> RR e. ( SubGrp ` CCfld ) ) |
| 16 |
14 15
|
ax-mp |
|- RR e. ( SubGrp ` CCfld ) |
| 17 |
16
|
a1i |
|- ( T. -> RR e. ( SubGrp ` CCfld ) ) |
| 18 |
5 10 12 17
|
efsubm |
|- ( T. -> ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) |
| 19 |
18
|
mptru |
|- ran ( x e. RR |-> ( exp ` ( _i x. x ) ) ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) |
| 20 |
9 19
|
eqeltri |
|- C e. ( SubMnd ` ( mulGrp ` CCfld ) ) |