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	ffvelrnd	|- ( ph -> ( L ` A ) e. ( Base ` Z ) )
16	8 15	ffvelrnd	|- ( ph -> ( X ` ( L ` A ) ) e. CC )