Metamath Proof Explorer

Theorem efgh

Description: The exponential function of a scaled complex number is a group homomorphism from the group of complex numbers under addition to the set of complex numbers under multiplication. (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 11-May-2014) (Revised by Thierry Arnoux, 26-Jan-2020)

Ref Expression
Hypothesis efgh.1 
|- F = ( x e. X |-> ( exp ` ( A x. x ) ) )
Assertion efgh 
|- ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( F ` ( B + C ) ) = ( ( F ` B ) x. ( F ` C ) ) )

Proof

Step Hyp Ref Expression
1 efgh.1 
 |-  F = ( x e. X |-> ( exp ` ( A x. x ) ) )
2 simp1l 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> A e. CC )
3 simp1r 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> X e. ( SubGrp ` CCfld ) )
4 cnfldbas 
 |-  CC = ( Base ` CCfld )
5 4 subgss 
 |-  ( X e. ( SubGrp ` CCfld ) -> X C_ CC )
6 3 5 syl 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> X C_ CC )
7 simp2 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> B e. X )
8 6 7 sseldd 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> B e. CC )
9 simp3 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> C e. X )
10 6 9 sseldd 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> C e. CC )
11 2 8 10 adddid 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
12 11 fveq2d 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( exp ` ( A x. ( B + C ) ) ) = ( exp ` ( ( A x. B ) + ( A x. C ) ) ) )
13 2 8 mulcld 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( A x. B ) e. CC )
14 2 10 mulcld 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( A x. C ) e. CC )
15 efadd 
 |-  ( ( ( A x. B ) e. CC /\ ( A x. C ) e. CC ) -> ( exp ` ( ( A x. B ) + ( A x. C ) ) ) = ( ( exp ` ( A x. B ) ) x. ( exp ` ( A x. C ) ) ) )
16 13 14 15 syl2anc 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( exp ` ( ( A x. B ) + ( A x. C ) ) ) = ( ( exp ` ( A x. B ) ) x. ( exp ` ( A x. C ) ) ) )
17 12 16 eqtrd 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( exp ` ( A x. ( B + C ) ) ) = ( ( exp ` ( A x. B ) ) x. ( exp ` ( A x. C ) ) ) )
18 oveq2 
 |-  ( x = y -> ( A x. x ) = ( A x. y ) )
19 18 fveq2d 
 |-  ( x = y -> ( exp ` ( A x. x ) ) = ( exp ` ( A x. y ) ) )
20 19 cbvmptv 
 |-  ( x e. X |-> ( exp ` ( A x. x ) ) ) = ( y e. X |-> ( exp ` ( A x. y ) ) )
21 1 20 eqtri 
 |-  F = ( y e. X |-> ( exp ` ( A x. y ) ) )
22 oveq2 
 |-  ( y = ( B + C ) -> ( A x. y ) = ( A x. ( B + C ) ) )
23 22 fveq2d 
 |-  ( y = ( B + C ) -> ( exp ` ( A x. y ) ) = ( exp ` ( A x. ( B + C ) ) ) )
24 cnfldadd 
 |-  + = ( +g ` CCfld )
25 24 subgcl 
 |-  ( ( X e. ( SubGrp ` CCfld ) /\ B e. X /\ C e. X ) -> ( B + C ) e. X )
26 25 3adant1l 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( B + C ) e. X )
27 fvexd 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( exp ` ( A x. ( B + C ) ) ) e. _V )
28 21 23 26 27 fvmptd3 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( F ` ( B + C ) ) = ( exp ` ( A x. ( B + C ) ) ) )
29 oveq2 
 |-  ( y = B -> ( A x. y ) = ( A x. B ) )
30 29 fveq2d 
 |-  ( y = B -> ( exp ` ( A x. y ) ) = ( exp ` ( A x. B ) ) )
31 fvexd 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( exp ` ( A x. B ) ) e. _V )
32 21 30 7 31 fvmptd3 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( F ` B ) = ( exp ` ( A x. B ) ) )
33 oveq2 
 |-  ( y = C -> ( A x. y ) = ( A x. C ) )
34 33 fveq2d 
 |-  ( y = C -> ( exp ` ( A x. y ) ) = ( exp ` ( A x. C ) ) )
35 fvexd 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( exp ` ( A x. C ) ) e. _V )
36 21 34 9 35 fvmptd3 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( F ` C ) = ( exp ` ( A x. C ) ) )
37 32 36 oveq12d 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( ( F ` B ) x. ( F ` C ) ) = ( ( exp ` ( A x. B ) ) x. ( exp ` ( A x. C ) ) ) )
38 17 28 37 3eqtr4d 
 |-  ( ( ( A e. CC /\ X e. ( SubGrp ` CCfld ) ) /\ B e. X /\ C e. X ) -> ( F ` ( B + C ) ) = ( ( F ` B ) x. ( F ` C ) ) )