Step |
Hyp |
Ref |
Expression |
1 |
|
efabl.1 |
|- F = ( x e. X |-> ( exp ` ( A x. x ) ) ) |
2 |
|
efabl.2 |
|- G = ( ( mulGrp ` CCfld ) |`s ran F ) |
3 |
|
efabl.3 |
|- ( ph -> A e. CC ) |
4 |
|
efabl.4 |
|- ( ph -> X e. ( SubGrp ` CCfld ) ) |
5 |
|
eff |
|- exp : CC --> CC |
6 |
5
|
a1i |
|- ( ( ph /\ x e. X ) -> exp : CC --> CC ) |
7 |
3
|
adantr |
|- ( ( ph /\ x e. X ) -> A e. CC ) |
8 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
9 |
8
|
subgss |
|- ( X e. ( SubGrp ` CCfld ) -> X C_ CC ) |
10 |
4 9
|
syl |
|- ( ph -> X C_ CC ) |
11 |
10
|
sselda |
|- ( ( ph /\ x e. X ) -> x e. CC ) |
12 |
7 11
|
mulcld |
|- ( ( ph /\ x e. X ) -> ( A x. x ) e. CC ) |
13 |
6 12
|
ffvelrnd |
|- ( ( ph /\ x e. X ) -> ( exp ` ( A x. x ) ) e. CC ) |
14 |
13
|
ralrimiva |
|- ( ph -> A. x e. X ( exp ` ( A x. x ) ) e. CC ) |
15 |
1
|
rnmptss |
|- ( A. x e. X ( exp ` ( A x. x ) ) e. CC -> ran F C_ CC ) |
16 |
14 15
|
syl |
|- ( ph -> ran F C_ CC ) |
17 |
3
|
mul01d |
|- ( ph -> ( A x. 0 ) = 0 ) |
18 |
17
|
fveq2d |
|- ( ph -> ( exp ` ( A x. 0 ) ) = ( exp ` 0 ) ) |
19 |
|
ef0 |
|- ( exp ` 0 ) = 1 |
20 |
18 19
|
eqtrdi |
|- ( ph -> ( exp ` ( A x. 0 ) ) = 1 ) |
21 |
|
cnfld0 |
|- 0 = ( 0g ` CCfld ) |
22 |
21
|
subg0cl |
|- ( X e. ( SubGrp ` CCfld ) -> 0 e. X ) |
23 |
4 22
|
syl |
|- ( ph -> 0 e. X ) |
24 |
|
fvex |
|- ( exp ` ( A x. 0 ) ) e. _V |
25 |
|
oveq2 |
|- ( x = 0 -> ( A x. x ) = ( A x. 0 ) ) |
26 |
25
|
fveq2d |
|- ( x = 0 -> ( exp ` ( A x. x ) ) = ( exp ` ( A x. 0 ) ) ) |
27 |
1 26
|
elrnmpt1s |
|- ( ( 0 e. X /\ ( exp ` ( A x. 0 ) ) e. _V ) -> ( exp ` ( A x. 0 ) ) e. ran F ) |
28 |
23 24 27
|
sylancl |
|- ( ph -> ( exp ` ( A x. 0 ) ) e. ran F ) |
29 |
20 28
|
eqeltrrd |
|- ( ph -> 1 e. ran F ) |
30 |
1 2 3 4
|
efabl |
|- ( ph -> G e. Abel ) |
31 |
|
ablgrp |
|- ( G e. Abel -> G e. Grp ) |
32 |
30 31
|
syl |
|- ( ph -> G e. Grp ) |
33 |
32
|
3ad2ant1 |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> G e. Grp ) |
34 |
|
simp2 |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> x e. ran F ) |
35 |
|
eqid |
|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld ) |
36 |
35 8
|
mgpbas |
|- CC = ( Base ` ( mulGrp ` CCfld ) ) |
37 |
2 36
|
ressbas2 |
|- ( ran F C_ CC -> ran F = ( Base ` G ) ) |
38 |
16 37
|
syl |
|- ( ph -> ran F = ( Base ` G ) ) |
39 |
38
|
3ad2ant1 |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> ran F = ( Base ` G ) ) |
40 |
34 39
|
eleqtrd |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> x e. ( Base ` G ) ) |
41 |
|
simp3 |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> y e. ran F ) |
42 |
41 39
|
eleqtrd |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> y e. ( Base ` G ) ) |
43 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
44 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
45 |
43 44
|
grpcl |
|- ( ( G e. Grp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) ) |
46 |
33 40 42 45
|
syl3anc |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) ) |
47 |
4
|
mptexd |
|- ( ph -> ( x e. X |-> ( exp ` ( A x. x ) ) ) e. _V ) |
48 |
1 47
|
eqeltrid |
|- ( ph -> F e. _V ) |
49 |
|
rnexg |
|- ( F e. _V -> ran F e. _V ) |
50 |
|
cnfldmul |
|- x. = ( .r ` CCfld ) |
51 |
35 50
|
mgpplusg |
|- x. = ( +g ` ( mulGrp ` CCfld ) ) |
52 |
2 51
|
ressplusg |
|- ( ran F e. _V -> x. = ( +g ` G ) ) |
53 |
48 49 52
|
3syl |
|- ( ph -> x. = ( +g ` G ) ) |
54 |
53
|
3ad2ant1 |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> x. = ( +g ` G ) ) |
55 |
54
|
oveqd |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> ( x x. y ) = ( x ( +g ` G ) y ) ) |
56 |
46 55 39
|
3eltr4d |
|- ( ( ph /\ x e. ran F /\ y e. ran F ) -> ( x x. y ) e. ran F ) |
57 |
56
|
3expb |
|- ( ( ph /\ ( x e. ran F /\ y e. ran F ) ) -> ( x x. y ) e. ran F ) |
58 |
57
|
ralrimivva |
|- ( ph -> A. x e. ran F A. y e. ran F ( x x. y ) e. ran F ) |
59 |
|
cnring |
|- CCfld e. Ring |
60 |
35
|
ringmgp |
|- ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd ) |
61 |
|
cnfld1 |
|- 1 = ( 1r ` CCfld ) |
62 |
35 61
|
ringidval |
|- 1 = ( 0g ` ( mulGrp ` CCfld ) ) |
63 |
36 62 51
|
issubm |
|- ( ( mulGrp ` CCfld ) e. Mnd -> ( ran F e. ( SubMnd ` ( mulGrp ` CCfld ) ) <-> ( ran F C_ CC /\ 1 e. ran F /\ A. x e. ran F A. y e. ran F ( x x. y ) e. ran F ) ) ) |
64 |
59 60 63
|
mp2b |
|- ( ran F e. ( SubMnd ` ( mulGrp ` CCfld ) ) <-> ( ran F C_ CC /\ 1 e. ran F /\ A. x e. ran F A. y e. ran F ( x x. y ) e. ran F ) ) |
65 |
16 29 58 64
|
syl3anbrc |
|- ( ph -> ran F e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) |