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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑥 ) ) )
Assertion efgh ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐵 + 𝐶 ) ) = ( ( 𝐹 ‘ 𝐵 ) · ( 𝐹 ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 efgh.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑥 ) ) )
2 simp1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 simp1r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝑋 ∈ ( SubGrp ‘ ℂfld ) )
4 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
5 4 subgss ⊢ ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) → 𝑋 ⊆ ℂ )
6 3 5 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝑋 ⊆ ℂ )
7 simp2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
8 6 7 sseldd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
9 simp3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
10 6 9 sseldd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
11 2 8 10 adddid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )
12 11 fveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · ( 𝐵 + 𝐶 ) ) ) = ( exp ‘ ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) ) )
13 2 8 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
14 2 10 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
15 efadd ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ ( 𝐴 · 𝐶 ) ∈ ℂ ) → ( exp ‘ ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) ) = ( ( exp ‘ ( 𝐴 · 𝐵 ) ) · ( exp ‘ ( 𝐴 · 𝐶 ) ) ) )
16 13 14 15 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( exp ‘ ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) ) = ( ( exp ‘ ( 𝐴 · 𝐵 ) ) · ( exp ‘ ( 𝐴 · 𝐶 ) ) ) )
17 12 16 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · ( 𝐵 + 𝐶 ) ) ) = ( ( exp ‘ ( 𝐴 · 𝐵 ) ) · ( exp ‘ ( 𝐴 · 𝐶 ) ) ) )
18 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑦 ) )
19 18 fveq2d ⊢ ( 𝑥 = 𝑦 → ( exp ‘ ( 𝐴 · 𝑥 ) ) = ( exp ‘ ( 𝐴 · 𝑦 ) ) )
20 19 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑥 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑦 ) ) )
21 1 20 eqtri ⊢ 𝐹 = ( 𝑦 ∈ 𝑋 ↦ ( exp ‘ ( 𝐴 · 𝑦 ) ) )
22 oveq2 ⊢ ( 𝑦 = ( 𝐵 + 𝐶 ) → ( 𝐴 · 𝑦 ) = ( 𝐴 · ( 𝐵 + 𝐶 ) ) )
23 22 fveq2d ⊢ ( 𝑦 = ( 𝐵 + 𝐶 ) → ( exp ‘ ( 𝐴 · 𝑦 ) ) = ( exp ‘ ( 𝐴 · ( 𝐵 + 𝐶 ) ) ) )
24 cnfldadd ⊢ + = ( +g ‘ ℂfld )
25 24 subgcl ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 + 𝐶 ) ∈ 𝑋 )
26 25 3adant1l ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 + 𝐶 ) ∈ 𝑋 )
27 fvexd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · ( 𝐵 + 𝐶 ) ) ) ∈ V )
28 21 23 26 27 fvmptd3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐵 + 𝐶 ) ) = ( exp ‘ ( 𝐴 · ( 𝐵 + 𝐶 ) ) ) )
29 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝐵 ) )
30 29 fveq2d ⊢ ( 𝑦 = 𝐵 → ( exp ‘ ( 𝐴 · 𝑦 ) ) = ( exp ‘ ( 𝐴 · 𝐵 ) ) )
31 fvexd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · 𝐵 ) ) ∈ V )
32 21 30 7 31 fvmptd3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) = ( exp ‘ ( 𝐴 · 𝐵 ) ) )
33 oveq2 ⊢ ( 𝑦 = 𝐶 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝐶 ) )
34 33 fveq2d ⊢ ( 𝑦 = 𝐶 → ( exp ‘ ( 𝐴 · 𝑦 ) ) = ( exp ‘ ( 𝐴 · 𝐶 ) ) )
35 fvexd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( exp ‘ ( 𝐴 · 𝐶 ) ) ∈ V )
36 21 34 9 35 fvmptd3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐶 ) = ( exp ‘ ( 𝐴 · 𝐶 ) ) )
37 32 36 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐵 ) · ( 𝐹 ‘ 𝐶 ) ) = ( ( exp ‘ ( 𝐴 · 𝐵 ) ) · ( exp ‘ ( 𝐴 · 𝐶 ) ) ) )
38 17 28 37 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑋 ∈ ( SubGrp ‘ ℂfld ) ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐵 + 𝐶 ) ) = ( ( 𝐹 ‘ 𝐵 ) · ( 𝐹 ‘ 𝐶 ) ) )