Theorem 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	⊢ 𝑀 = ( mulGrp ‘ ℂfld )
	expghm.u	⊢ 𝑈 = ( 𝑀 ↾s ( ℂ ∖ { 0 } ) )
Assertion	expghm	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( ℤring GrpHom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		expghm.m	⊢ 𝑀 = ( mulGrp ‘ ℂfld )
2		expghm.u	⊢ 𝑈 = ( 𝑀 ↾s ( ℂ ∖ { 0 } ) )
3		expclzlem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑥 ∈ ℤ ) → ( 𝐴 ↑ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
4	3	3expa	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℤ ) → ( 𝐴 ↑ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
5	4	fmpttd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) : ℤ ⟶ ( ℂ ∖ { 0 } ) )
6		expaddz	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) = ( ( 𝐴 ↑ 𝑦 ) · ( 𝐴 ↑ 𝑧 ) ) )
7		zaddcl	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑦 + 𝑧 ) ∈ ℤ )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 + 𝑧 ) ∈ ℤ )
9		oveq2	⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) )
10		eqid	⊢ ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) )
11		ovex	⊢ ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) ∈ V
12	9 10 11	fvmpt	⊢ ( ( 𝑦 + 𝑧 ) ∈ ℤ → ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) )
13	8 12	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) )
14		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑦 ) )
15		ovex	⊢ ( 𝐴 ↑ 𝑦 ) ∈ V
16	14 10 15	fvmpt	⊢ ( 𝑦 ∈ ℤ → ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) = ( 𝐴 ↑ 𝑦 ) )
17		oveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑧 ) )
18		ovex	⊢ ( 𝐴 ↑ 𝑧 ) ∈ V
19	17 10 18	fvmpt	⊢ ( 𝑧 ∈ ℤ → ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) = ( 𝐴 ↑ 𝑧 ) )
20	16 19	oveqan12d	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) = ( ( 𝐴 ↑ 𝑦 ) · ( 𝐴 ↑ 𝑧 ) ) )
21	20	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) = ( ( 𝐴 ↑ 𝑦 ) · ( 𝐴 ↑ 𝑧 ) ) )
22	6 13 21	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) )
23	22	ralrimivva	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ∀ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ℤ ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) )
24		zringgrp	⊢ ℤring ∈ Grp
25		cnring	⊢ ℂfld ∈ Ring
26		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
27		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
28		cndrng	⊢ ℂfld ∈ DivRing
29	26 27 28	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
30	1	oveq1i	⊢ ( 𝑀 ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
31	2 30	eqtri	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
32	29 31	unitgrp	⊢ ( ℂfld ∈ Ring → 𝑈 ∈ Grp )
33	25 32	ax-mp	⊢ 𝑈 ∈ Grp
34	24 33	pm3.2i	⊢ ( ℤring ∈ Grp ∧ 𝑈 ∈ Grp )
35		zringbas	⊢ ℤ = ( Base ‘ ℤring )
36		difss	⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
37	1 26	mgpbas	⊢ ℂ = ( Base ‘ 𝑀 )
38	2 37	ressbas2	⊢ ( ( ℂ ∖ { 0 } ) ⊆ ℂ → ( ℂ ∖ { 0 } ) = ( Base ‘ 𝑈 ) )
39	36 38	ax-mp	⊢ ( ℂ ∖ { 0 } ) = ( Base ‘ 𝑈 )
40		zringplusg	⊢ + = ( +g ‘ ℤring )
41	29	fvexi	⊢ ( ℂ ∖ { 0 } ) ∈ V
42		cnfldmul	⊢ · = ( .r ‘ ℂfld )
43	1 42	mgpplusg	⊢ · = ( +g ‘ 𝑀 )
44	2 43	ressplusg	⊢ ( ( ℂ ∖ { 0 } ) ∈ V → · = ( +g ‘ 𝑈 ) )
45	41 44	ax-mp	⊢ · = ( +g ‘ 𝑈 )
46	35 39 40 45	isghm	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( ℤring GrpHom 𝑈 ) ↔ ( ( ℤring ∈ Grp ∧ 𝑈 ∈ Grp ) ∧ ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) : ℤ ⟶ ( ℂ ∖ { 0 } ) ∧ ∀ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ℤ ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) ) ) )
47	34 46	mpbiran	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( ℤring GrpHom 𝑈 ) ↔ ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) : ℤ ⟶ ( ℂ ∖ { 0 } ) ∧ ∀ 𝑦 ∈ ℤ ∀ 𝑧 ∈ ℤ ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) ) )
48	5 23 47	sylanbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( ℤring GrpHom 𝑈 ) )