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โ„ค โ€˜ ๐‘› ) / ๐‘ง โฆŒ โฆ‹ { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ง ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } ) โІ ๐‘ฅ } / ๐‘ โฆŒ { โŸจ ( Base โ€˜ ndx ) , ๐‘ โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) ) โŸฉ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdchr โŠข DChr
1 vn โŠข ๐‘›
2 cn โŠข โ„•
3 czn โŠข โ„ค/nโ„ค
4 1 cv โŠข ๐‘›
5 4 3 cfv โŠข ( โ„ค/nโ„ค โ€˜ ๐‘› )
6 vz โŠข ๐‘ง
7 vx โŠข ๐‘ฅ
8 cmgp โŠข mulGrp
9 6 cv โŠข ๐‘ง
10 9 8 cfv โŠข ( mulGrp โ€˜ ๐‘ง )
11 cmhm โŠข MndHom
12 ccnfld โŠข โ„‚fld
13 12 8 cfv โŠข ( mulGrp โ€˜ โ„‚fld )
14 10 13 11 co โŠข ( ( mulGrp โ€˜ ๐‘ง ) MndHom ( mulGrp โ€˜ โ„‚fld ) )
15 cbs โŠข Base
16 9 15 cfv โŠข ( Base โ€˜ ๐‘ง )
17 cui โŠข Unit
18 9 17 cfv โŠข ( Unit โ€˜ ๐‘ง )
19 16 18 cdif โŠข ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) )
20 cc0 โŠข 0
21 20 csn โŠข { 0 }
22 19 21 cxp โŠข ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } )
23 7 cv โŠข ๐‘ฅ
24 22 23 wss โŠข ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } ) โІ ๐‘ฅ
25 24 7 14 crab โŠข { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ง ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } ) โІ ๐‘ฅ }
26 vb โŠข ๐‘
27 cnx โŠข ndx
28 27 15 cfv โŠข ( Base โ€˜ ndx )
29 26 cv โŠข ๐‘
30 28 29 cop โŠข โŸจ ( Base โ€˜ ndx ) , ๐‘ โŸฉ
31 cplusg โŠข +g
32 27 31 cfv โŠข ( +g โ€˜ ndx )
33 cmul โŠข ยท
34 33 cof โŠข โˆ˜f ยท
35 29 29 cxp โŠข ( ๐‘ ร— ๐‘ )
36 34 35 cres โŠข ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) )
37 32 36 cop โŠข โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) ) โŸฉ
38 30 37 cpr โŠข { โŸจ ( Base โ€˜ ndx ) , ๐‘ โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) ) โŸฉ }
39 26 25 38 csb โŠข โฆ‹ { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ง ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } ) โІ ๐‘ฅ } / ๐‘ โฆŒ { โŸจ ( Base โ€˜ ndx ) , ๐‘ โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) ) โŸฉ }
40 6 5 39 csb โŠข โฆ‹ ( โ„ค/nโ„ค โ€˜ ๐‘› ) / ๐‘ง โฆŒ โฆ‹ { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ง ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } ) โІ ๐‘ฅ } / ๐‘ โฆŒ { โŸจ ( Base โ€˜ ndx ) , ๐‘ โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) ) โŸฉ }
41 1 2 40 cmpt โŠข ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( โ„ค/nโ„ค โ€˜ ๐‘› ) / ๐‘ง โฆŒ โฆ‹ { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ง ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } ) โІ ๐‘ฅ } / ๐‘ โฆŒ { โŸจ ( Base โ€˜ ndx ) , ๐‘ โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) ) โŸฉ } )
42 0 41 wceq โŠข DChr = ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( โ„ค/nโ„ค โ€˜ ๐‘› ) / ๐‘ง โฆŒ โฆ‹ { ๐‘ฅ โˆˆ ( ( mulGrp โ€˜ ๐‘ง ) MndHom ( mulGrp โ€˜ โ„‚fld ) ) โˆฃ ( ( ( Base โ€˜ ๐‘ง ) โˆ– ( Unit โ€˜ ๐‘ง ) ) ร— { 0 } ) โІ ๐‘ฅ } / ๐‘ โฆŒ { โŸจ ( Base โ€˜ ndx ) , ๐‘ โŸฉ , โŸจ ( +g โ€˜ ndx ) , ( โˆ˜f ยท โ†พ ( ๐‘ ร— ๐‘ ) ) โŸฉ } )