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

Metamath Proof Explorer

Theorem dchrzrhcl

Description: A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses dchrmhm.g 
|- G = ( DChr ` N )
dchrmhm.z 
|- Z = ( Z/nZ ` N )
dchrmhm.b 
|- D = ( Base ` G )
dchrelbas4.l 
|- L = ( ZRHom ` Z )
dchrzrh1.x 
|- ( ph -> X e. D )
dchrzrh1.a 
|- ( ph -> A e. ZZ )
Assertion dchrzrhcl 
|- ( ph -> ( X ` ( L ` A ) ) e. CC )

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 dchrelbas4.l 
 |-  L = ( ZRHom ` Z )
5 dchrzrh1.x 
 |-  ( ph -> X e. D )
6 dchrzrh1.a 
 |-  ( ph -> A e. ZZ )
7 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
8 1 2 3 7 5 dchrf 
 |-  ( ph -> X : ( Base ` Z ) --> CC )
9 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
10 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
11 5 9 10 3syl 
 |-  ( ph -> N e. NN0 )
12 2 7 4 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
13 fof 
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
14 11 12 13 3syl 
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
15 14 6 ffvelcdmd 
 |-  ( ph -> ( L ` A ) e. ( Base ` Z ) )
16 8 15 ffvelcdmd 
 |-  ( ph -> ( X ` ( L ` A ) ) e. CC )