Theorem dchrmhm

Description: A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-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$$
Assertion	dchrmhm	$$⊢D\subseteq {\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$

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		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
5		eqid	$$⊢\mathrm{Unit}\left(Z\right)=\mathrm{Unit}\left(Z\right)$$
6	1 3	dchrrcl	$$⊢x\in D\to N\in \mathbb{N}$$
7	1 2 4 5 6 3	dchrelbas	$$⊢x\in D\to \left(x\in D\leftrightarrow \left(x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left({\mathrm{Base}}_Z\setminus \mathrm{Unit}\left(Z\right)\right)\times \left\{0\right\}\subseteq x\right)\right)$$
8	7	ibi	$$⊢x\in D\to \left(x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left({\mathrm{Base}}_Z\setminus \mathrm{Unit}\left(Z\right)\right)\times \left\{0\right\}\subseteq x\right)$$
9	8	simpld	$$⊢x\in D\to x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
10	9	ssriv	$$⊢D\subseteq {\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$