expghm

Description: Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	expghm.m	$⊢ M = {mulGrp}_{ℂ_{fld}}$
	expghm.u	$⊢ U = M ↾_{𝑠} (ℂ ∖ \{0\})$
Assertion	expghm	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℤ ⟼ A^{x}) \in (ℤ_{ring} GrpHom U)$

Proof

Step	Hyp	Ref	Expression
1		expghm.m	$⊢ M = {mulGrp}_{ℂ_{fld}}$
2		expghm.u	$⊢ U = M ↾_{𝑠} (ℂ ∖ \{0\})$
3		expclzlem	$⊢ (A \in ℂ \land A \neq 0 \land x \in ℤ) \to A^{x} \in (ℂ ∖ \{0\})$
4	3	3expa	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℤ) \to A^{x} \in (ℂ ∖ \{0\})$
5	4	fmpttd	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℤ ⟼ A^{x}) : ℤ ⟶ ℂ ∖ \{0\}$
6		expaddz	$⊢ ((A \in ℂ \land A \neq 0) \land (y \in ℤ \land z \in ℤ)) \to A^{y + z} = A^{y} A^{z}$
7		zaddcl	$⊢ (y \in ℤ \land z \in ℤ) \to y + z \in ℤ$
8	7	adantl	$⊢ ((A \in ℂ \land A \neq 0) \land (y \in ℤ \land z \in ℤ)) \to y + z \in ℤ$
9		oveq2	$⊢ x = y + z \to A^{x} = A^{y + z}$
10		eqid	$⊢ (x \in ℤ ⟼ A^{x}) = (x \in ℤ ⟼ A^{x})$
11		ovex	$⊢ A^{y + z} \in V$
12	9 10 11	fvmpt	$⊢ y + z \in ℤ \to (x \in ℤ ⟼ A^{x}) (y + z) = A^{y + z}$
13	8 12	syl	$⊢ ((A \in ℂ \land A \neq 0) \land (y \in ℤ \land z \in ℤ)) \to (x \in ℤ ⟼ A^{x}) (y + z) = A^{y + z}$
14		oveq2	$⊢ x = y \to A^{x} = A^{y}$
15		ovex	$⊢ A^{y} \in V$
16	14 10 15	fvmpt	$⊢ y \in ℤ \to (x \in ℤ ⟼ A^{x}) (y) = A^{y}$
17		oveq2	$⊢ x = z \to A^{x} = A^{z}$
18		ovex	$⊢ A^{z} \in V$
19	17 10 18	fvmpt	$⊢ z \in ℤ \to (x \in ℤ ⟼ A^{x}) (z) = A^{z}$
20	16 19	oveqan12d	$⊢ (y \in ℤ \land z \in ℤ) \to (x \in ℤ ⟼ A^{x}) (y) (x \in ℤ ⟼ A^{x}) (z) = A^{y} A^{z}$
21	20	adantl	$⊢ ((A \in ℂ \land A \neq 0) \land (y \in ℤ \land z \in ℤ)) \to (x \in ℤ ⟼ A^{x}) (y) (x \in ℤ ⟼ A^{x}) (z) = A^{y} A^{z}$
22	6 13 21	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (y \in ℤ \land z \in ℤ)) \to (x \in ℤ ⟼ A^{x}) (y + z) = (x \in ℤ ⟼ A^{x}) (y) (x \in ℤ ⟼ A^{x}) (z)$
23	22	ralrimivva	$⊢ (A \in ℂ \land A \neq 0) \to \forall y \in ℤ \forall z \in ℤ (x \in ℤ ⟼ A^{x}) (y + z) = (x \in ℤ ⟼ A^{x}) (y) (x \in ℤ ⟼ A^{x}) (z)$
24		zringgrp	$⊢ ℤ_{ring} \in Grp$
25		cnring	$⊢ ℂ_{fld} \in Ring$
26		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
27		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
28		cndrng	$⊢ ℂ_{fld} \in DivRing$
29	26 27 28	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
30	1	oveq1i	$⊢ M ↾_{𝑠} (ℂ ∖ \{0\}) = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
31	2 30	eqtri	$⊢ U = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
32	29 31	unitgrp	$⊢ ℂ_{fld} \in Ring \to U \in Grp$
33	25 32	ax-mp	$⊢ U \in Grp$
34	24 33	pm3.2i	$⊢ (ℤ_{ring} \in Grp \land U \in Grp)$
35		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
36		difss	$⊢ ℂ ∖ \{0\} \subseteq ℂ$
37	1 26	mgpbas	$⊢ ℂ = {Base}_{M}$
38	2 37	ressbas2	$⊢ ℂ ∖ \{0\} \subseteq ℂ \to ℂ ∖ \{0\} = {Base}_{U}$
39	36 38	ax-mp	$⊢ ℂ ∖ \{0\} = {Base}_{U}$
40		zringplusg	$⊢ + = +_{ℤ_{ring}}$
41	29	fvexi	$⊢ ℂ ∖ \{0\} \in V$
42		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
43	1 42	mgpplusg	$⊢ \times = +_{M}$
44	2 43	ressplusg	$⊢ ℂ ∖ \{0\} \in V \to \times = +_{U}$
45	41 44	ax-mp	$⊢ \times = +_{U}$
46	35 39 40 45	isghm	$⊢ (x \in ℤ ⟼ A^{x}) \in (ℤ_{ring} GrpHom U) \leftrightarrow ((ℤ_{ring} \in Grp \land U \in Grp) \land ((x \in ℤ ⟼ A^{x}) : ℤ ⟶ ℂ ∖ \{0\} \land \forall y \in ℤ \forall z \in ℤ (x \in ℤ ⟼ A^{x}) (y + z) = (x \in ℤ ⟼ A^{x}) (y) (x \in ℤ ⟼ A^{x}) (z)))$
47	34 46	mpbiran	$⊢ (x \in ℤ ⟼ A^{x}) \in (ℤ_{ring} GrpHom U) \leftrightarrow ((x \in ℤ ⟼ A^{x}) : ℤ ⟶ ℂ ∖ \{0\} \land \forall y \in ℤ \forall z \in ℤ (x \in ℤ ⟼ A^{x}) (y + z) = (x \in ℤ ⟼ A^{x}) (y) (x \in ℤ ⟼ A^{x}) (z))$
48	5 23 47	sylanbrc	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℤ ⟼ A^{x}) \in (ℤ_{ring} GrpHom U)$

Metamath Proof Explorer

Theorem expghm

Proof