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 ∈ X ⟼ e A ⁢ x
Assertion efgh ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → F ⁡ B + C = F ⁡ B ⁢ F ⁡ C

Proof

Step Hyp Ref Expression
1 efgh.1 ⊢ F = x ∈ X ⟼ e A ⁢ x
2 simp1l ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → A ∈ ℂ
3 simp1r ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → X ∈ SubGrp ⁡ ℂ fld
4 cnfldbas ⊢ ℂ = Base ℂ fld
5 4 subgss ⊢ X ∈ SubGrp ⁡ ℂ fld → X ⊆ ℂ
6 3 5 syl ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → X ⊆ ℂ
7 simp2 ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → B ∈ X
8 6 7 sseldd ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → B ∈ ℂ
9 simp3 ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → C ∈ X
10 6 9 sseldd ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → C ∈ ℂ
11 2 8 10 adddid ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → A ⁢ B + C = A ⁢ B + A ⁢ C
12 11 fveq2d ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → e A ⁢ B + C = e A ⁢ B + A ⁢ C
13 2 8 mulcld ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → A ⁢ B ∈ ℂ
14 2 10 mulcld ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → A ⁢ C ∈ ℂ
15 efadd ⊢ A ⁢ B ∈ ℂ ∧ A ⁢ C ∈ ℂ → e A ⁢ B + A ⁢ C = e A ⁢ B ⁢ e A ⁢ C
16 13 14 15 syl2anc ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → e A ⁢ B + A ⁢ C = e A ⁢ B ⁢ e A ⁢ C
17 12 16 eqtrd ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → e A ⁢ B + C = e A ⁢ B ⁢ e A ⁢ C
18 oveq2 ⊢ x = y → A ⁢ x = A ⁢ y
19 18 fveq2d ⊢ x = y → e A ⁢ x = e A ⁢ y
20 19 cbvmptv ⊢ x ∈ X ⟼ e A ⁢ x = y ∈ X ⟼ e A ⁢ y
21 1 20 eqtri ⊢ F = y ∈ X ⟼ e A ⁢ y
22 oveq2 ⊢ y = B + C → A ⁢ y = A ⁢ B + C
23 22 fveq2d ⊢ y = B + C → e A ⁢ y = e A ⁢ B + C
24 cnfldadd ⊢ + = + ℂ fld
25 24 subgcl ⊢ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → B + C ∈ X
26 25 3adant1l ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → B + C ∈ X
27 fvexd ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → e A ⁢ B + C ∈ V
28 21 23 26 27 fvmptd3 ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → F ⁡ B + C = e A ⁢ B + C
29 oveq2 ⊢ y = B → A ⁢ y = A ⁢ B
30 29 fveq2d ⊢ y = B → e A ⁢ y = e A ⁢ B
31 fvexd ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → e A ⁢ B ∈ V
32 21 30 7 31 fvmptd3 ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → F ⁡ B = e A ⁢ B
33 oveq2 ⊢ y = C → A ⁢ y = A ⁢ C
34 33 fveq2d ⊢ y = C → e A ⁢ y = e A ⁢ C
35 fvexd ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → e A ⁢ C ∈ V
36 21 34 9 35 fvmptd3 ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → F ⁡ C = e A ⁢ C
37 32 36 oveq12d ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → F ⁡ B ⁢ F ⁡ C = e A ⁢ B ⁢ e A ⁢ C
38 17 28 37 3eqtr4d ⊢ A ∈ ℂ ∧ X ∈ SubGrp ⁡ ℂ fld ∧ B ∈ X ∧ C ∈ X → F ⁡ B + C = F ⁡ B ⁢ F ⁡ C