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 X e A x
efabl.2 G = mulGrp fld 𝑠 ran F
efabl.3 φ A
efabl.4 φ X SubGrp fld
Assertion efabl φ G Abel

Proof

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