# Metamath Proof Explorer

## 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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cdchr ${class}\mathrm{DChr}$
1 vn ${setvar}{n}$
2 cn ${class}ℕ$
3 czn ${class}\mathrm{ℤ/nℤ}$
4 1 cv ${setvar}{n}$
5 4 3 cfv ${class}ℤ/{n}ℤ$
6 vz ${setvar}{z}$
7 vx ${setvar}{x}$
8 cmgp ${class}\mathrm{mulGrp}$
9 6 cv ${setvar}{z}$
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 ${class}0$
21 20 csn ${class}\left\{0\right\}$
22 19 21 cxp ${class}\left(\left({\mathrm{Base}}_{{z}}\setminus \mathrm{Unit}\left({z}\right)\right)×\left\{0\right\}\right)$
23 7 cv ${setvar}{x}$
24 22 23 wss ${wff}\left({\mathrm{Base}}_{{z}}\setminus \mathrm{Unit}\left({z}\right)\right)×\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)×\left\{0\right\}\subseteq {x}\right\}$
26 vb ${setvar}{b}$
27 cnx ${class}\mathrm{ndx}$
28 27 15 cfv ${class}{\mathrm{Base}}_{\mathrm{ndx}}$
29 26 cv ${setvar}{b}$
30 28 29 cop ${class}⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩$
31 cplusg ${class}{+}_{𝑔}$
32 27 31 cfv ${class}{+}_{\mathrm{ndx}}$
33 cmul ${class}×$
34 33 cof ${class}{\circ }_{f}×$
35 29 29 cxp ${class}\left({b}×{b}\right)$
36 34 35 cres ${class}\left({{\circ }_{f}×↾}_{\left({b}×{b}\right)}\right)$
37 32 36 cop ${class}⟨{+}_{\mathrm{ndx}},{{\circ }_{f}×↾}_{\left({b}×{b}\right)}⟩$
38 30 37 cpr ${class}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_{f}×↾}_{\left({b}×{b}\right)}⟩\right\}$
39 26 25 38 csb
40 6 5 39 csb
41 1 2 40 cmpt
42 0 41 wceq