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