Definition df-dchr 24958

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

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 ) , ( oF x. |` ( b X. b ) ) >. } )

Distinct variable groups:   x, z   n, b, z, x

Detailed syntax breakdown of Definition df-dchr

Step	Hyp	Ref	Expression
1		cdchr 24957	. 2 class DChr
2		vn	. . 3 setvar n
3		cn 11020	. . 3 class NN
4		vz	. . . 4 setvar z
5	2	cv 1482	. . . . 5 class n
6		czn 19851	. . . . 5 class ℤ/nℤ
7	5, 6	cfv 5888	. . . 4 class (ℤ/nℤ ` n )
8		vb	. . . . 5 setvar b
9	4	cv 1482	. . . . . . . . . 10 class z
10		cbs 15857	. . . . . . . . . 10 class Base
11	9, 10	cfv 5888	. . . . . . . . 9 class ( Base ` z )
12		cui 18639	. . . . . . . . . 10 class Unit
13	9, 12	cfv 5888	. . . . . . . . 9 class (Unit ` z )
14	11, 13	cdif 3571	. . . . . . . 8 class ( ( Base ` z ) \ (Unit ` z ) )
15		cc0 9936	. . . . . . . . 9 class 0
16	15	csn 4177	. . . . . . . 8 class { 0 }
17	14, 16	cxp 5112	. . . . . . 7 class ( ( ( Base ` z ) \ (Unit ` z ) ) X. { 0 } )
18		vx	. . . . . . . 8 setvar x
19	18	cv 1482	. . . . . . 7 class x
20	17, 19	wss 3574	. . . . . 6 wff ( ( ( Base ` z ) \ (Unit ` z ) ) X. { 0 } ) C_ x
21		cmgp 18489	. . . . . . . 8 class mulGrp
22	9, 21	cfv 5888	. . . . . . 7 class (mulGrp ` z )
23		ccnfld 19746	. . . . . . . 8 class ℂfld
24	23, 21	cfv 5888	. . . . . . 7 class (mulGrp ` ℂfld )
25		cmhm 17333	. . . . . . 7 class MndHom
26	22, 24, 25	co 6650	. . . . . 6 class ( (mulGrp ` z ) MndHom (mulGrp ` ℂfld ) )
27	20, 18, 26	crab 2916	. . . . 5 class { x e. ( (mulGrp ` z ) MndHom (mulGrp ` ℂfld ) ) | ( ( ( Base ` z ) \ (Unit ` z ) ) X. { 0 } ) C_ x }
28		cnx 15854	. . . . . . . 8 class ndx
29	28, 10	cfv 5888	. . . . . . 7 class ( Base ` ndx )
30	8	cv 1482	. . . . . . 7 class b
31	29, 30	cop 4183	. . . . . 6 class <. ( Base ` ndx ) , b >.
32		cplusg 15941	. . . . . . . 8 class +g
33	28, 32	cfv 5888	. . . . . . 7 class ( +g ` ndx )
34		cmul 9941	. . . . . . . . 9 class x.
35	34	cof 6895	. . . . . . . 8 class oF x.
36	30, 30	cxp 5112	. . . . . . . 8 class ( b X. b )
37	35, 36	cres 5116	. . . . . . 7 class ( oF x. |` ( b X. b ) )
38	33, 37	cop 4183	. . . . . 6 class <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >.
39	31, 38	cpr 4179	. . . . 5 class { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. }
40	8, 27, 39	csb 3533	. . . 4 class [_ { x e. ( (mulGrp ` z ) MndHom (mulGrp ` ℂfld ) ) | ( ( ( Base ` z ) \ (Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. }
41	4, 7, 40	csb 3533	. . 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 ) , ( oF x. |` ( b X. b ) ) >. }
42	2, 3, 41	cmpt 4729	. 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 ) , ( oF x. |` ( b X. b ) ) >. } )
43	1, 42	wceq 1483	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 ) , ( oF x. |` ( b X. b ) ) >. } )

This definition is referenced by:  dchrval  24959  dchrrcl  24965