Metamath Proof Explorer

Theorem efabl

Description: The image of a subgroup of the group + , under the exponential function of a scaled complex number, is an Abelian group. (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 26-Jan-2020)

Ref Expression
Hypotheses efabl.1 
|- F = ( x e. X |-> ( exp ` ( A x. x ) ) )
efabl.2 
|- G = ( ( mulGrp ` CCfld ) |`s ran F )
efabl.3 
|- ( ph -> A e. CC )
efabl.4 
|- ( ph -> X e. ( SubGrp ` CCfld ) )
Assertion efabl 
|- ( ph -> G e. Abel )

Proof

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 eqid 
 |-  ( Base ` ( CCfld |`s X ) ) = ( Base ` ( CCfld |`s X ) )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 eqid 
 |-  ( +g ` ( CCfld |`s X ) ) = ( +g ` ( CCfld |`s X ) )
8 eqid 
 |-  ( +g ` G ) = ( +g ` G )
9 simp1 
 |-  ( ( ph /\ x e. ( Base ` ( CCfld |`s X ) ) /\ y e. ( Base ` ( CCfld |`s X ) ) ) -> ph )
10 simp2 
 |-  ( ( ph /\ x e. ( Base ` ( CCfld |`s X ) ) /\ y e. ( Base ` ( CCfld |`s X ) ) ) -> x e. ( Base ` ( CCfld |`s X ) ) )
11 eqid 
 |-  ( CCfld |`s X ) = ( CCfld |`s X )
12 11 subgbas 
 |-  ( X e. ( SubGrp ` CCfld ) -> X = ( Base ` ( CCfld |`s X ) ) )
13 4 12 syl 
 |-  ( ph -> X = ( Base ` ( CCfld |`s X ) ) )
14 13 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` ( CCfld |`s X ) ) /\ y e. ( Base ` ( CCfld |`s X ) ) ) -> X = ( Base ` ( CCfld |`s X ) ) )
15 10 14 eleqtrrd 
 |-  ( ( ph /\ x e. ( Base ` ( CCfld |`s X ) ) /\ y e. ( Base ` ( CCfld |`s X ) ) ) -> x e. X )
16 simp3 
 |-  ( ( ph /\ x e. ( Base ` ( CCfld |`s X ) ) /\ y e. ( Base ` ( CCfld |`s X ) ) ) -> y e. ( Base ` ( CCfld |`s X ) ) )
17 16 14 eleqtrrd 
 |-  ( ( ph /\ x e. ( Base ` ( CCfld |`s X ) ) /\ y e. ( Base ` ( CCfld |`s X ) ) ) -> y e. X )
18 3 4 jca 
 |-  ( ph -> ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) )
19 1 efgh 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ x e. X /\ y e. X ) -> ( F ` ( x + y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
20 18 19 syl3an1 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x + y ) ) = ( ( F ` x ) x. ( F ` y ) ) )
21 cnfldadd 
 |-  + = ( +g ` CCfld )
22 11 21 ressplusg 
 |-  ( X e. ( SubGrp ` CCfld ) -> + = ( +g ` ( CCfld |`s X ) ) )
23 4 22 syl 
 |-  ( ph -> + = ( +g ` ( CCfld |`s X ) ) )
24 23 3ad2ant1 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> + = ( +g ` ( CCfld |`s X ) ) )
25 24 oveqd 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( x + y ) = ( x ( +g ` ( CCfld |`s X ) ) y ) )
26 25 fveq2d 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x + y ) ) = ( F ` ( x ( +g ` ( CCfld |`s X ) ) y ) ) )
27 mptexg 
 |-  ( X e. ( SubGrp ` CCfld ) -> ( x e. X |-> ( exp ` ( A x. x ) ) ) e. _V )
28 1 27 eqeltrid 
 |-  ( X e. ( SubGrp ` CCfld ) -> F e. _V )
29 rnexg 
 |-  ( F e. _V -> ran F e. _V )
30 4 28 29 3syl 
 |-  ( ph -> ran F e. _V )
31 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
32 cnfldmul 
 |-  x. = ( .r ` CCfld )
33 31 32 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
34 2 33 ressplusg 
 |-  ( ran F e. _V -> x. = ( +g ` G ) )
35 30 34 syl 
 |-  ( ph -> x. = ( +g ` G ) )
36 35 3ad2ant1 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> x. = ( +g ` G ) )
37 36 oveqd 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( ( F ` x ) x. ( F ` y ) ) = ( ( F ` x ) ( +g ` G ) ( F ` y ) ) )
38 20 26 37 3eqtr3d 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x ( +g ` ( CCfld |`s X ) ) y ) ) = ( ( F ` x ) ( +g ` G ) ( F ` y ) ) )
39 9 15 17 38 syl3anc 
 |-  ( ( ph /\ x e. ( Base ` ( CCfld |`s X ) ) /\ y e. ( Base ` ( CCfld |`s X ) ) ) -> ( F ` ( x ( +g ` ( CCfld |`s X ) ) y ) ) = ( ( F ` x ) ( +g ` G ) ( F ` y ) ) )
40 fvex 
 |-  ( exp ` ( A x. x ) ) e. _V
41 40 1 fnmpti 
 |-  F Fn X
42 dffn4 
 |-  ( F Fn X <-> F : X -onto-> ran F )
43 41 42 mpbi 
 |-  F : X -onto-> ran F
44 eqidd 
 |-  ( ph -> F = F )
45 eff 
 |-  exp : CC --> CC
46 45 a1i 
 |-  ( ( ph /\ x e. X ) -> exp : CC --> CC )
47 3 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
48 cnfldbas 
 |-  CC = ( Base ` CCfld )
49 48 subgss 
 |-  ( X e. ( SubGrp ` CCfld ) -> X C_ CC )
50 4 49 syl 
 |-  ( ph -> X C_ CC )
51 50 sselda 
 |-  ( ( ph /\ x e. X ) -> x e. CC )
52 47 51 mulcld 
 |-  ( ( ph /\ x e. X ) -> ( A x. x ) e. CC )
53 46 52 ffvelrnd 
 |-  ( ( ph /\ x e. X ) -> ( exp ` ( A x. x ) ) e. CC )
54 53 ralrimiva 
 |-  ( ph -> A. x e. X ( exp ` ( A x. x ) ) e. CC )
55 1 rnmptss 
 |-  ( A. x e. X ( exp ` ( A x. x ) ) e. CC -> ran F C_ CC )
56 31 48 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
57 2 56 ressbas2 
 |-  ( ran F C_ CC -> ran F = ( Base ` G ) )
58 54 55 57 3syl 
 |-  ( ph -> ran F = ( Base ` G ) )
59 44 13 58 foeq123d 
 |-  ( ph -> ( F : X -onto-> ran F <-> F : ( Base ` ( CCfld |`s X ) ) -onto-> ( Base ` G ) ) )
60 43 59 mpbii 
 |-  ( ph -> F : ( Base ` ( CCfld |`s X ) ) -onto-> ( Base ` G ) )
61 cnring 
 |-  CCfld e. Ring
62 ringabl 
 |-  ( CCfld e. Ring -> CCfld e. Abel )
63 61 62 ax-mp 
 |-  CCfld e. Abel
64 11 subgabl 
 |-  ( ( CCfld e. Abel /\ X e. ( SubGrp ` CCfld ) ) -> ( CCfld |`s X ) e. Abel )
65 63 4 64 sylancr 
 |-  ( ph -> ( CCfld |`s X ) e. Abel )
66 5 6 7 8 39 60 65 ghmabl 
 |-  ( ph -> G e. Abel )