Theorem dchrelbas

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrval.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrval.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrval.b	$$⊢B={\mathrm{Base}}_Z$$
	dchrval.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	dchrval.n	$$⊢\phi \to N\in \mathbb{N}$$
	dchrbas.b	$$⊢D={\mathrm{Base}}_G$$
Assertion	dchrelbas	$$⊢\phi \to \left(X\in D\leftrightarrow \left(X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left(B\setminus U\right)\times \left\{0\right\}\subseteq X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dchrval.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrval.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchrval.b	$$⊢B={\mathrm{Base}}_Z$$
4		dchrval.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
5		dchrval.n	$$⊢\phi \to N\in \mathbb{N}$$
6		dchrbas.b	$$⊢D={\mathrm{Base}}_G$$
7	1 2 3 4 5 6	dchrbas	$$⊢\phi \to D=\left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}$$
8	7	eleq2d	$$⊢\phi \to \left(X\in D\leftrightarrow X\in \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\right)$$
9		sseq2	$$⊢x=X\to \left(\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\leftrightarrow \left(B\setminus U\right)\times \left\{0\right\}\subseteq X\right)$$
10	9	elrab	$$⊢X\in \left\{x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left(B\setminus U\right)\times \left\{0\right\}\subseteq x\right\}\leftrightarrow \left(X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left(B\setminus U\right)\times \left\{0\right\}\subseteq X\right)$$
11	8 10	bitrdi	$$⊢\phi \to \left(X\in D\leftrightarrow \left(X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left(B\setminus U\right)\times \left\{0\right\}\subseteq X\right)\right)$$