Theorem dchrzrhmul

Description: A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrmhm.b	$$⊢D={\mathrm{Base}}_G$$
	dchrelbas4.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
	dchrzrh1.x	$$⊢\phi \to X\in D$$
	dchrzrh1.a	$$⊢\phi \to A\in \mathbb{Z}$$
	dchrzrh1.c	$$⊢\phi \to C\in \mathbb{Z}$$
Assertion	dchrzrhmul	$$⊢\phi \to X\left(L\left(AC\right)\right)=X\left(L\left(A\right)\right)X\left(L\left(C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchrmhm.b	$$⊢D={\mathrm{Base}}_G$$
4		dchrelbas4.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
5		dchrzrh1.x	$$⊢\phi \to X\in D$$
6		dchrzrh1.a	$$⊢\phi \to A\in \mathbb{Z}$$
7		dchrzrh1.c	$$⊢\phi \to C\in \mathbb{Z}$$
8	1 3	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
9	5 8	syl	$$⊢\phi \to N\in \mathbb{N}$$
10	9	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11	2	zncrng	$$⊢N\in {\mathbb{N}}_0\to Z\in \mathrm{CRing}$$
12	10 11	syl	$$⊢\phi \to Z\in \mathrm{CRing}$$
13		crngring	$$⊢Z\in \mathrm{CRing}\to Z\in \mathrm{Ring}$$
14	12 13	syl	$$⊢\phi \to Z\in \mathrm{Ring}$$
15	4	zrhrhm	$$⊢Z\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Z\right)$$
16	14 15	syl	$$⊢\phi \to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Z\right)$$
17		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
18		zringmulr	$$⊢\times ={\cdot }_{{\mathbb{Z}}_{\mathrm{ring}}}$$
19		eqid	$$⊢{\cdot }_Z={\cdot }_Z$$
20	17 18 19	rhmmul	$$⊢\left(L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Z\right)\wedge A\in \mathbb{Z}\wedge C\in \mathbb{Z}\right)\to L\left(AC\right)=L\left(A\right){\cdot }_{Z}L\left(C\right)$$
21	16 6 7 20	syl3anc	$$⊢\phi \to L\left(AC\right)=L\left(A\right){\cdot }_{Z}L\left(C\right)$$
22	21	fveq2d	$$⊢\phi \to X\left(L\left(AC\right)\right)=X\left(L\left(A\right){\cdot }_{Z}L\left(C\right)\right)$$
23	1 2 3	dchrmhm	$$⊢D\subseteq {\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
24	23 5	sselid	$$⊢\phi \to X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
25		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
26	17 25	rhmf	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}Z\right)\to L:\mathbb{Z}⟶{\mathrm{Base}}_Z$$
27	16 26	syl	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_Z$$
28	27 6	ffvelcdmd	$$⊢\phi \to L\left(A\right)\in {\mathrm{Base}}_Z$$
29	27 7	ffvelcdmd	$$⊢\phi \to L\left(C\right)\in {\mathrm{Base}}_Z$$
30		eqid	$$⊢{\mathrm{mulGrp}}_Z={\mathrm{mulGrp}}_Z$$
31	30 25	mgpbas	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}$$
32	30 19	mgpplusg	$$⊢{\cdot }_Z={+}_{{\mathrm{mulGrp}}_Z}$$
33		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
34		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
35	33 34	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
36	31 32 35	mhmlin	$$⊢\left(X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge L\left(A\right)\in {\mathrm{Base}}_Z\wedge L\left(C\right)\in {\mathrm{Base}}_Z\right)\to X\left(L\left(A\right){\cdot }_{Z}L\left(C\right)\right)=X\left(L\left(A\right)\right)X\left(L\left(C\right)\right)$$
37	24 28 29 36	syl3anc	$$⊢\phi \to X\left(L\left(A\right){\cdot }_{Z}L\left(C\right)\right)=X\left(L\left(A\right)\right)X\left(L\left(C\right)\right)$$
38	22 37	eqtrd	$$⊢\phi \to X\left(L\left(AC\right)\right)=X\left(L\left(A\right)\right)X\left(L\left(C\right)\right)$$