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
|- DChr = ( n e. NN |-> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdchr
 |-  DChr
1 vn
 |-  n
2 cn
 |-  NN
3 czn
 |-  Z/nZ
4 1 cv
 |-  n
5 4 3 cfv
 |-  ( Z/nZ ` n )
6 vz
 |-  z
7 vx
 |-  x
8 cmgp
 |-  mulGrp
9 6 cv
 |-  z
10 9 8 cfv
 |-  ( mulGrp ` z )
11 cmhm
 |-  MndHom
12 ccnfld
 |-  CCfld
13 12 8 cfv
 |-  ( mulGrp ` CCfld )
14 10 13 11 co
 |-  ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) )
15 cbs
 |-  Base
16 9 15 cfv
 |-  ( Base ` z )
17 cui
 |-  Unit
18 9 17 cfv
 |-  ( Unit ` z )
19 16 18 cdif
 |-  ( ( Base ` z ) \ ( Unit ` z ) )
20 cc0
 |-  0
21 20 csn
 |-  { 0 }
22 19 21 cxp
 |-  ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } )
23 7 cv
 |-  x
24 22 23 wss
 |-  ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x
25 24 7 14 crab
 |-  { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x }
26 vb
 |-  b
27 cnx
 |-  ndx
28 27 15 cfv
 |-  ( Base ` ndx )
29 26 cv
 |-  b
30 28 29 cop
 |-  <. ( Base ` ndx ) , b >.
31 cplusg
 |-  +g
32 27 31 cfv
 |-  ( +g ` ndx )
33 cmul
 |-  x.
34 33 cof
 |-  oF x.
35 29 29 cxp
 |-  ( b X. b )
36 34 35 cres
 |-  ( oF x. |` ( b X. b ) )
37 32 36 cop
 |-  <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >.
38 30 37 cpr
 |-  { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. }
39 26 25 38 csb
 |-  [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. }
40 6 5 39 csb
 |-  [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. }
41 1 2 40 cmpt
 |-  ( n e. NN |-> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } )
42 0 41 wceq
 |-  DChr = ( n e. NN |-> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } )