Metamath Proof Explorer


Theorem dchrelbas

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g
|- G = ( DChr ` N )
dchrval.z
|- Z = ( Z/nZ ` N )
dchrval.b
|- B = ( Base ` Z )
dchrval.u
|- U = ( Unit ` Z )
dchrval.n
|- ( ph -> N e. NN )
dchrbas.b
|- D = ( Base ` G )
Assertion dchrelbas
|- ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) )

Proof

Step Hyp Ref Expression
1 dchrval.g
 |-  G = ( DChr ` N )
2 dchrval.z
 |-  Z = ( Z/nZ ` N )
3 dchrval.b
 |-  B = ( Base ` Z )
4 dchrval.u
 |-  U = ( Unit ` Z )
5 dchrval.n
 |-  ( ph -> N e. NN )
6 dchrbas.b
 |-  D = ( Base ` G )
7 1 2 3 4 5 6 dchrbas
 |-  ( ph -> D = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )
8 7 eleq2d
 |-  ( ph -> ( X e. D <-> X e. { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } ) )
9 sseq2
 |-  ( x = X -> ( ( ( B \ U ) X. { 0 } ) C_ x <-> ( ( B \ U ) X. { 0 } ) C_ X ) )
10 9 elrab
 |-  ( X e. { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) )
11 8 10 bitrdi
 |-  ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) )