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

Theorem efgh 20445
 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 9081 . . . 4
21fveq2d 5734 . . 3
3 mulcl 9076 . . . . 5
433adant3 978 . . . 4
5 mulcl 9076 . . . . 5
653adant2 977 . . . 4
7 efadd 12698 . . . 4
84, 6, 7syl2anc 644 . . 3
92, 8eqtrd 2470 . 2
10 addcl 9074 . . . 4
12 oveq2 6091 . . . . 5
1312fveq2d 5734 . . . 4
14 efgh.1 . . . 4
15 fvex 5744 . . . 4
1613, 14, 15fvmpt 5808 . . 3
1711, 16syl 16 . 2
18 oveq2 6091 . . . . . 6
1918fveq2d 5734 . . . . 5
20 fvex 5744 . . . . 5
2119, 14, 20fvmpt 5808 . . . 4
22 oveq2 6091 . . . . . 6
2322fveq2d 5734 . . . . 5
24 fvex 5744 . . . . 5
2523, 14, 24fvmpt 5808 . . . 4
2621, 25oveqan12d 6102 . . 3