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=\mathrm{DChr}\left(N\right)$$
	dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrmhm.b	$$⊢D={\mathrm{Base}}_G$$
	dchrelbas4.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
	dchrzrh1.x	$$⊢\phi \to X\in D$$
	dchrzrh1.a	$$⊢\phi \to A\in \mathbb{Z}$$
Assertion	dchrzrhcl	$$⊢\phi \to X\left(L\left(A\right)\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchrmhm.b	$$⊢D={\mathrm{Base}}_G$$
4		dchrelbas4.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
5		dchrzrh1.x	$$⊢\phi \to X\in D$$
6		dchrzrh1.a	$$⊢\phi \to A\in \mathbb{Z}$$
7		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
8	1 2 3 7 5	dchrf	$$⊢\phi \to X:{\mathrm{Base}}_Z⟶ℂ$$
9	1 3	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
10		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
11	5 9 10	3syl	$$⊢\phi \to N\in {\mathbb{N}}_0$$
12	2 7 4	znzrhfo	$$⊢N\in {\mathbb{N}}_0\to L:\mathbb{Z}\underset{onto}{⟶}{\mathrm{Base}}_Z$$
13		fof	$$⊢L:\mathbb{Z}\underset{onto}{⟶}{\mathrm{Base}}_Z\to L:\mathbb{Z}⟶{\mathrm{Base}}_Z$$
14	11 12 13	3syl	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_Z$$
15	14 6	ffvelrnd	$$⊢\phi \to L\left(A\right)\in {\mathrm{Base}}_Z$$
16	8 15	ffvelrnd	$$⊢\phi \to X\left(L\left(A\right)\right)\in ℂ$$