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 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 efsubm
|- ( ph -> ran F e. ( SubMnd ` ( mulGrp ` CCfld ) ) )

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 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 ) ) )