Metamath Proof Explorer

Theorem dchrmhm

Description: A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g 
|- G = ( DChr ` N )
dchrmhm.z 
|- Z = ( Z/nZ ` N )
dchrmhm.b 
|- D = ( Base ` G )
Assertion dchrmhm 
|- D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g 
 |-  G = ( DChr ` N )
2 dchrmhm.z 
 |-  Z = ( Z/nZ ` N )
3 dchrmhm.b 
 |-  D = ( Base ` G )
4 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
5 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
6 1 3 dchrrcl 
 |-  ( x e. D -> N e. NN )
7 1 2 4 5 6 3 dchrelbas 
 |-  ( x e. D -> ( x e. D <-> ( x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( ( Base ` Z ) \ ( Unit ` Z ) ) X. { 0 } ) C_ x ) ) )
8 7 ibi 
 |-  ( x e. D -> ( x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( ( Base ` Z ) \ ( Unit ` Z ) ) X. { 0 } ) C_ x ) )
9 8 simpld 
 |-  ( x e. D -> x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
10 9 ssriv 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )