Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgh Unicode version

Theorem efgh 19735
 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.)
Hypothesis
Ref Expression
efgh.1
Assertion
Ref Expression
efgh
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem efgh
StepHypRef Expression
1 adddi 8706 . . . 4
21fveq2d 5381 . . 3
3 mulcl 8701 . . . . 5
433adant3 980 . . . 4
5 mulcl 8701 . . . . 5
653adant2 979 . . . 4
7 efadd 12249 . . . 4
84, 6, 7syl2anc 645 . . 3
92, 8eqtrd 2285 . 2
10 addcl 8699 . . . 4
12 oveq2 5718 . . . . 5
1312fveq2d 5381 . . . 4
14 efgh.1 . . . 4
15 fvex 5391 . . . 4
1613, 14, 15fvmpt 5454 . . 3
1711, 16syl 17 . 2
18 oveq2 5718 . . . . . 6
1918fveq2d 5381 . . . . 5
20 fvex 5391 . . . . 5
2119, 14, 20fvmpt 5454 . . . 4
22 oveq2 5718 . . . . . 6
2322fveq2d 5381 . . . . 5
24 fvex 5391 . . . . 5
2523, 14, 24fvmpt 5454 . . . 4
2621, 25oveqan12d 5729 . . 3