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	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℕ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 𝑀 ) )