Definition df-dchr

Description: The group of Dirichlet characters mod n is the set of monoid homomorphisms from ZZ / n ZZ to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Assertion	df-dchr	$$⊢\mathrm{DChr}=\left(n\in \mathbb{N}⟼⦋\mathbb{Z}/n\mathbb{Z}/z⦌⦋\left\{x\in \left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x\right\}/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdchr	$$class\mathrm{DChr}$$
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3		czn	$$class\mathrm{\mathbb{Z}/n\mathbb{Z}}$$
4	1	cv	$$setvarn$$
5	4 3	cfv	$$class\mathbb{Z}/n\mathbb{Z}$$
6		vz	$$setvarz$$
7		vx	$$setvarx$$
8		cmgp	$$class\mathrm{mulGrp}$$
9	6	cv	$$setvarz$$
10	9 8	cfv	$$class{\mathrm{mulGrp}}_z$$
11		cmhm	$$class\mathrm{MndHom}$$
12		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
13	12 8	cfv	$$class{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
14	10 13 11	co	$$class\left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
15		cbs	$$class\mathrm{Base}$$
16	9 15	cfv	$$class{\mathrm{Base}}_z$$
17		cui	$$class\mathrm{Unit}$$
18	9 17	cfv	$$class\mathrm{Unit}\left(z\right)$$
19	16 18	cdif	$$class\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)$$
20		cc0	$$class0$$
21	20	csn	$$class\left\{0\right\}$$
22	19 21	cxp	$$class\left(\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\right)$$
23	7	cv	$$setvarx$$
24	22 23	wss	$$wff\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x$$
25	24 7 14	crab	$$class\left\{x\in \left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x\right\}$$
26		vb	$$setvarb$$
27		cnx	$$class\mathrm{ndx}$$
28	27 15	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
29	26	cv	$$setvarb$$
30	28 29	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩$$
31		cplusg	$$class{+}_{𝑔}$$
32	27 31	cfv	$$class{+}_{\mathrm{ndx}}$$
33		cmul	$$class\times$$
34	33	cof	$$class{\circ }_f\times$$
35	29 29	cxp	$$class\left(b\times b\right)$$
36	34 35	cres	$$class\left({{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}\right)$$
37	32 36	cop	$$class⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩$$
38	30 37	cpr	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩\right\}$$
39	26 25 38	csb	$$class⦋\left\{x\in \left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x\right\}/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩\right\}$$
40	6 5 39	csb	$$class⦋\mathbb{Z}/n\mathbb{Z}/z⦌⦋\left\{x\in \left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x\right\}/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩\right\}$$
41	1 2 40	cmpt	$$class\left(n\in \mathbb{N}⟼⦋\mathbb{Z}/n\mathbb{Z}/z⦌⦋\left\{x\in \left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x\right\}/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩\right\}\right)$$
42	0 41	wceq	$$wff\mathrm{DChr}=\left(n\in \mathbb{N}⟼⦋\mathbb{Z}/n\mathbb{Z}/z⦌⦋\left\{x\in \left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x\right\}/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩\right\}\right)$$