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 ) ) >. } )