This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem expmhm

Description: Exponentiation is a monoid homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses expmhm.1 ⊢ 𝑁 = ( ℂfld ↾s ℕ0 )
expmhm.2 ⊢ 𝑀 = ( mulGrp ‘ ℂfld )
Assertion expmhm ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( 𝑁 MndHom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 expmhm.1 ⊢ 𝑁 = ( ℂfld ↾s ℕ0 )
2 expmhm.2 ⊢ 𝑀 = ( mulGrp ‘ ℂfld )
3 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑥 ) ∈ ℂ )
4 3 fmpttd ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) : ℕ0 ⟶ ℂ )
5 expadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) = ( ( 𝐴 ↑ 𝑦 ) · ( 𝐴 ↑ 𝑧 ) ) )
6 5 3expb ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) = ( ( 𝐴 ↑ 𝑦 ) · ( 𝐴 ↑ 𝑧 ) ) )
7 nn0addcl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) → ( 𝑦 + 𝑧 ) ∈ ℕ0 )
8 7 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( 𝑦 + 𝑧 ) ∈ ℕ0 )
9 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) )
10 eqid ⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) )
11 ovex ⊢ ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) ∈ V
12 9 10 11 fvmpt ⊢ ( ( 𝑦 + 𝑧 ) ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) )
13 8 12 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( 𝐴 ↑ ( 𝑦 + 𝑧 ) ) )
14 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑦 ) )
15 ovex ⊢ ( 𝐴 ↑ 𝑦 ) ∈ V
16 14 10 15 fvmpt ⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) = ( 𝐴 ↑ 𝑦 ) )
17 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 𝑧 ) )
18 ovex ⊢ ( 𝐴 ↑ 𝑧 ) ∈ V
19 17 10 18 fvmpt ⊢ ( 𝑧 ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) = ( 𝐴 ↑ 𝑧 ) )
20 16 19 oveqan12d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) → ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) = ( ( 𝐴 ↑ 𝑦 ) · ( 𝐴 ↑ 𝑧 ) ) )
21 20 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) = ( ( 𝐴 ↑ 𝑦 ) · ( 𝐴 ↑ 𝑧 ) ) )
22 6 13 21 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ ℕ0 ) ) → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) )
23 22 ralrimivva ⊢ ( 𝐴 ∈ ℂ → ∀ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) )
24 0nn0 ⊢ 0 ∈ ℕ0
25 oveq2 ⊢ ( 𝑥 = 0 → ( 𝐴 ↑ 𝑥 ) = ( 𝐴 ↑ 0 ) )
26 ovex ⊢ ( 𝐴 ↑ 0 ) ∈ V
27 25 10 26 fvmpt ⊢ ( 0 ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 0 ) = ( 𝐴 ↑ 0 ) )
28 24 27 ax-mp ⊢ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 0 ) = ( 𝐴 ↑ 0 )
29 exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
30 28 29 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 0 ) = 1 )
31 nn0subm ⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
32 1 submmnd ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 𝑁 ∈ Mnd )
33 31 32 ax-mp ⊢ 𝑁 ∈ Mnd
34 cnring ⊢ ℂfld ∈ Ring
35 2 ringmgp ⊢ ( ℂfld ∈ Ring → 𝑀 ∈ Mnd )
36 34 35 ax-mp ⊢ 𝑀 ∈ Mnd
37 33 36 pm3.2i ⊢ ( 𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd )
38 1 submbas ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ℕ0 = ( Base ‘ 𝑁 ) )
39 31 38 ax-mp ⊢ ℕ0 = ( Base ‘ 𝑁 )
40 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
41 2 40 mgpbas ⊢ ℂ = ( Base ‘ 𝑀 )
42 cnfldadd ⊢ + = ( +g ‘ ℂfld )
43 1 42 ressplusg ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → + = ( +g ‘ 𝑁 ) )
44 31 43 ax-mp ⊢ + = ( +g ‘ 𝑁 )
45 cnfldmul ⊢ · = ( .r ‘ ℂfld )
46 2 45 mgpplusg ⊢ · = ( +g ‘ 𝑀 )
47 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
48 1 47 subm0 ⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 0 = ( 0g ‘ 𝑁 ) )
49 31 48 ax-mp ⊢ 0 = ( 0g ‘ 𝑁 )
50 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
51 2 50 ringidval ⊢ 1 = ( 0g ‘ 𝑀 )
52 39 41 44 46 49 51 ismhm ⊢ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( 𝑁 MndHom 𝑀 ) ↔ ( ( 𝑁 ∈ Mnd ∧ 𝑀 ∈ Mnd ) ∧ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) : ℕ0 ⟶ ℂ ∧ ∀ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) ∧ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 0 ) = 1 ) ) )
53 37 52 mpbiran ⊢ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( 𝑁 MndHom 𝑀 ) ↔ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) : ℕ0 ⟶ ℂ ∧ ∀ 𝑦 ∈ ℕ0 ∀ 𝑧 ∈ ℕ0 ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ ( 𝑦 + 𝑧 ) ) = ( ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑦 ) · ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 𝑧 ) ) ∧ ( ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ‘ 0 ) = 1 ) )
54 4 23 30 53 syl3anbrc ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑥 ) ) ∈ ( 𝑁 MndHom 𝑀 ) )