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 \in X ⟼ e^{A x})$
	Assertion	efgh	$⊢ ((A \in ℂ \land X \in SubGrp (ℂ_{fld})) \land B \in X \land C \in X) \to F (B + C) = F (B) F (C)$

Proof

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

Metamath Proof Explorer

Theorem efgh

Proof