MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dchr Unicode version

Definition df-dchr 20472
Description: The group of Dirichlet characters  mod  n is the set of monoid homomorphisms from  ZZ  /  n ZZ to the multiplicative monoid of the complexes, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016.)
Assertion
Ref Expression
df-dchr  |- DChr  =  ( n  e.  NN  |->  [_ (ℤ/n `  n )  /  z ]_ [_ { x  e.  ( (mulGrp `  z
) MndHom  (mulGrp ` fld ) )  |  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  o F  x.  |`  ( b  X.  b ) )
>. } )
Distinct variable groups:    x, z    n, b, z, x

Detailed syntax breakdown of Definition df-dchr
StepHypRef Expression
1 cdchr 20471 . 2  class DChr
2 vn . . 3  set  n
3 cn 9746 . . 3  class  NN
4 vz . . . 4  set  z
52cv 1622 . . . . 5  class  n
6 czn 16454 . . . . 5  class ℤ/n
75, 6cfv 5255 . . . 4  class  (ℤ/n `  n
)
8 vb . . . . 5  set  b
94cv 1622 . . . . . . . . . 10  class  z
10 cbs 13148 . . . . . . . . . 10  class  Base
119, 10cfv 5255 . . . . . . . . 9  class  ( Base `  z )
12 cui 15421 . . . . . . . . . 10  class Unit
139, 12cfv 5255 . . . . . . . . 9  class  (Unit `  z )
1411, 13cdif 3149 . . . . . . . 8  class  ( (
Base `  z )  \  (Unit `  z )
)
15 cc0 8737 . . . . . . . . 9  class  0
1615csn 3640 . . . . . . . 8  class  { 0 }
1714, 16cxp 4687 . . . . . . 7  class  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )
18 vx . . . . . . . 8  set  x
1918cv 1622 . . . . . . 7  class  x
2017, 19wss 3152 . . . . . 6  wff  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x
21 cmgp 15325 . . . . . . . 8  class mulGrp
229, 21cfv 5255 . . . . . . 7  class  (mulGrp `  z )
23 ccnfld 16377 . . . . . . . 8  classfld
2423, 21cfv 5255 . . . . . . 7  class  (mulGrp ` fld )
25 cmhm 14413 . . . . . . 7  class MndHom
2622, 24, 25co 5858 . . . . . 6  class  ( (mulGrp `  z ) MndHom  (mulGrp ` fld )
)
2720, 18, 26crab 2547 . . . . 5  class  { x  e.  ( (mulGrp `  z
) MndHom  (mulGrp ` fld ) )  |  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x }
28 cnx 13145 . . . . . . . 8  class  ndx
2928, 10cfv 5255 . . . . . . 7  class  ( Base `  ndx )
308cv 1622 . . . . . . 7  class  b
3129, 30cop 3643 . . . . . 6  class  <. ( Base `  ndx ) ,  b >.
32 cplusg 13208 . . . . . . . 8  class  +g
3328, 32cfv 5255 . . . . . . 7  class  ( +g  ` 
ndx )
34 cmul 8742 . . . . . . . . 9  class  x.
3534cof 6076 . . . . . . . 8  class  o F  x.
3630, 30cxp 4687 . . . . . . . 8  class  ( b  X.  b )
3735, 36cres 4691 . . . . . . 7  class  (  o F  x.  |`  (
b  X.  b ) )
3833, 37cop 3643 . . . . . 6  class  <. ( +g  `  ndx ) ,  (  o F  x.  |`  ( b  X.  b
) ) >.
3931, 38cpr 3641 . . . . 5  class  { <. (
Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  (  o F  x.  |`  ( b  X.  b
) ) >. }
408, 27, 39csb 3081 . . . 4  class  [_ {
x  e.  ( (mulGrp `  z ) MndHom  (mulGrp ` fld )
)  |  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  o F  x.  |`  ( b  X.  b ) )
>. }
414, 7, 40csb 3081 . . 3  class  [_ (ℤ/n `  n
)  /  z ]_ [_ { x  e.  ( (mulGrp `  z ) MndHom  (mulGrp ` fld ) )  |  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  o F  x.  |`  ( b  X.  b ) )
>. }
422, 3, 41cmpt 4077 . 2  class  ( n  e.  NN  |->  [_ (ℤ/n `  n
)  /  z ]_ [_ { x  e.  ( (mulGrp `  z ) MndHom  (mulGrp ` fld ) )  |  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  o F  x.  |`  ( b  X.  b ) )
>. } )
431, 42wceq 1623 1  wff DChr  =  ( n  e.  NN  |->  [_ (ℤ/n `  n )  /  z ]_ [_ { x  e.  ( (mulGrp `  z
) MndHom  (mulGrp ` fld ) )  |  ( ( ( Base `  z
)  \  (Unit `  z
) )  X.  {
0 } )  C_  x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  (  o F  x.  |`  ( b  X.  b ) )
>. } )
Colors of variables: wff set class
This definition is referenced by:  dchrval  20473  dchrrcl  20479
  Copyright terms: Public domain W3C validator