Metamath Proof Explorer


Theorem efsubm

Description: The image of a subgroup of the group + , under the exponential function of a scaled complex number is a submonoid of the multiplicative group of CCfld . (Contributed 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 efsubm φ ran F SubMnd mulGrp fld

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