This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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