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