Theorem dchrzrh1

Description: Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-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$$
Assertion	dchrzrh1	$$⊢\phi \to X\left(L\left(1\right)\right)=1$$

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	1 3	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
7	5 6	syl	$$⊢\phi \to N\in \mathbb{N}$$
8	7	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9	2	zncrng	$$⊢N\in {\mathbb{N}}_0\to Z\in \mathrm{CRing}$$
10		crngring	$$⊢Z\in \mathrm{CRing}\to Z\in \mathrm{Ring}$$
11		eqid	$$⊢1_Z=1_Z$$
12	4 11	zrh1	$$⊢Z\in \mathrm{Ring}\to L\left(1\right)=1_Z$$
13	8 9 10 12	4syl	$$⊢\phi \to L\left(1\right)=1_Z$$
14	13	fveq2d	$$⊢\phi \to X\left(L\left(1\right)\right)=X\left(1_Z\right)$$
15	1 2 3	dchrmhm	$$⊢D\subseteq {\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
16	15 5	sseldi	$$⊢\phi \to X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
17		eqid	$$⊢{\mathrm{mulGrp}}_Z={\mathrm{mulGrp}}_Z$$
18	17 11	ringidval	$$⊢1_Z=0_{{\mathrm{mulGrp}}_Z}$$
19		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
20		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
21	19 20	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
22	18 21	mhm0	$$⊢X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\to X\left(1_Z\right)=1$$
23	16 22	syl	$$⊢\phi \to X\left(1_Z\right)=1$$
24	14 23	eqtrd	$$⊢\phi \to X\left(L\left(1\right)\right)=1$$