Theorem expmhm

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

	Ref	Expression
Hypotheses	expmhm.1	$$⊢N={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
	expmhm.2	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
Assertion	expmhm	$$⊢A\in ℂ\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\in \left(N\mathrm{MndHom}M\right)$$

Proof

Step	Hyp	Ref	Expression
1		expmhm.1	$$⊢N={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
2		expmhm.2	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
3		expcl	$$⊢\left(A\in ℂ\wedge x\in {\mathbb{N}}_0\right)\to A^x\in ℂ$$
4	3	fmpttd	$$⊢A\in ℂ\to \left(x\in {\mathbb{N}}_0⟼A^x\right):{\mathbb{N}}_0⟶ℂ$$
5		expadd	$$⊢\left(A\in ℂ\wedge y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\to A^{y+z}=A^y{A}^z$$
6	5	3expb	$$⊢\left(A\in ℂ\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to A^{y+z}=A^y{A}^z$$
7		nn0addcl	$$⊢\left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\to y+z\in {\mathbb{N}}_0$$
8	7	adantl	$$⊢\left(A\in ℂ\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to y+z\in {\mathbb{N}}_0$$
9		oveq2	$$⊢x=y+z\to A^x=A^{y+z}$$
10		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼A^x\right)=\left(x\in {\mathbb{N}}_0⟼A^x\right)$$
11		ovex	$$⊢A^{y+z}\in \mathrm{V}$$
12	9 10 11	fvmpt	$$⊢y+z\in {\mathbb{N}}_0\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y+z\right)=A^{y+z}$$
13	8 12	syl	$$⊢\left(A\in ℂ\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y+z\right)=A^{y+z}$$
14		oveq2	$$⊢x=y\to A^x=A^y$$
15		ovex	$$⊢A^y\in \mathrm{V}$$
16	14 10 15	fvmpt	$$⊢y\in {\mathbb{N}}_0\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y\right)=A^y$$
17		oveq2	$$⊢x=z\to A^x=A^z$$
18		ovex	$$⊢A^z\in \mathrm{V}$$
19	17 10 18	fvmpt	$$⊢z\in {\mathbb{N}}_0\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(z\right)=A^z$$
20	16 19	oveqan12d	$$⊢\left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y\right)\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(z\right)=A^y{A}^z$$
21	20	adantl	$$⊢\left(A\in ℂ\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y\right)\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(z\right)=A^y{A}^z$$
22	6 13 21	3eqtr4d	$$⊢\left(A\in ℂ\wedge \left(y\in {\mathbb{N}}_0\wedge z\in {\mathbb{N}}_0\right)\right)\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y+z\right)=\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y\right)\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(z\right)$$
23	22	ralrimivva	$$⊢A\in ℂ\to \forall y\in {\mathbb{N}}_0\forall z\in {\mathbb{N}}_0\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y+z\right)=\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y\right)\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(z\right)$$
24		0nn0	$$⊢0\in {\mathbb{N}}_0$$
25		oveq2	$$⊢x=0\to A^x=A^0$$
26		ovex	$$⊢A^0\in \mathrm{V}$$
27	25 10 26	fvmpt	$$⊢0\in {\mathbb{N}}_0\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(0\right)=A^0$$
28	24 27	ax-mp	$$⊢\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(0\right)=A^0$$
29		exp0	$$⊢A\in ℂ\to A^0=1$$
30	28 29	syl5eq	$$⊢A\in ℂ\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(0\right)=1$$
31		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
32	1	submmnd	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to N\in \mathrm{Mnd}$$
33	31 32	ax-mp	$$⊢N\in \mathrm{Mnd}$$
34		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
35	2	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to M\in \mathrm{Mnd}$$
36	34 35	ax-mp	$$⊢M\in \mathrm{Mnd}$$
37	33 36	pm3.2i	$$⊢\left(N\in \mathrm{Mnd}\wedge M\in \mathrm{Mnd}\right)$$
38	1	submbas	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {\mathbb{N}}_0={\mathrm{Base}}_N$$
39	31 38	ax-mp	$$⊢{\mathbb{N}}_0={\mathrm{Base}}_N$$
40		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
41	2 40	mgpbas	$$⊢ℂ={\mathrm{Base}}_M$$
42		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
43	1 42	ressplusg	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to +={+}_N$$
44	31 43	ax-mp	$$⊢+={+}_N$$
45		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
46	2 45	mgpplusg	$$⊢\times ={+}_M$$
47		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
48	1 47	subm0	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_N$$
49	31 48	ax-mp	$$⊢0=0_N$$
50		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
51	2 50	ringidval	$$⊢1=0_M$$
52	39 41 44 46 49 51	ismhm	$$⊢\left(x\in {\mathbb{N}}_0⟼A^x\right)\in \left(N\mathrm{MndHom}M\right)\leftrightarrow \left(\left(N\in \mathrm{Mnd}\wedge M\in \mathrm{Mnd}\right)\wedge \left(\left(x\in {\mathbb{N}}_0⟼A^x\right):{\mathbb{N}}_0⟶ℂ\wedge \forall y\in {\mathbb{N}}_0\forall z\in {\mathbb{N}}_0\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y+z\right)=\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y\right)\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(z\right)\wedge \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(0\right)=1\right)\right)$$
53	37 52	mpbiran	$$⊢\left(x\in {\mathbb{N}}_0⟼A^x\right)\in \left(N\mathrm{MndHom}M\right)\leftrightarrow \left(\left(x\in {\mathbb{N}}_0⟼A^x\right):{\mathbb{N}}_0⟶ℂ\wedge \forall y\in {\mathbb{N}}_0\forall z\in {\mathbb{N}}_0\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y+z\right)=\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(y\right)\left(x\in {\mathbb{N}}_0⟼A^x\right)\left(z\right)\wedge \left(x\in {\mathbb{N}}_0⟼A^x\right)\left(0\right)=1\right)$$
54	4 23 30 53	syl3anbrc	$$⊢A\in ℂ\to \left(x\in {\mathbb{N}}_0⟼A^x\right)\in \left(N\mathrm{MndHom}M\right)$$