Metamath Proof Explorer

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 𝑈 ) )