Theorem dchrsum

Description: An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrsum.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrsum.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrsum.d	$$⊢D={\mathrm{Base}}_G$$
	dchrsum.1	$$⊢\underset{\dot{}}{1}=0_G$$
	dchrsum.x	$$⊢\phi \to X\in D$$
	dchrsum.b	$$⊢B={\mathrm{Base}}_Z$$
Assertion	dchrsum	$$⊢\phi \to \sum _{a\in B}X\left(a\right)=if\left(X=\underset{\dot{}}{1},\mathrm{\varphi }\left(N\right),0\right)$$

Proof

Step	Hyp	Ref	Expression
1		dchrsum.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrsum.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchrsum.d	$$⊢D={\mathrm{Base}}_G$$
4		dchrsum.1	$$⊢\underset{\dot{}}{1}=0_G$$
5		dchrsum.x	$$⊢\phi \to X\in D$$
6		dchrsum.b	$$⊢B={\mathrm{Base}}_Z$$
7		eqid	$$⊢\mathrm{Unit}\left(Z\right)=\mathrm{Unit}\left(Z\right)$$
8	6 7	unitss	$$⊢\mathrm{Unit}\left(Z\right)\subseteq B$$
9	8	a1i	$$⊢\phi \to \mathrm{Unit}\left(Z\right)\subseteq B$$
10	1 2 3 6 5	dchrf	$$⊢\phi \to X:B⟶ℂ$$
11	8	sseli	$$⊢a\in \mathrm{Unit}\left(Z\right)\to a\in B$$
12		ffvelcdm	$$⊢\left(X:B⟶ℂ\wedge a\in B\right)\to X\left(a\right)\in ℂ$$
13	10 11 12	syl2an	$$⊢\left(\phi \wedge a\in \mathrm{Unit}\left(Z\right)\right)\to X\left(a\right)\in ℂ$$
14		eldif	$$⊢a\in \left(B\setminus \mathrm{Unit}\left(Z\right)\right)\leftrightarrow \left(a\in B\wedge \neg a\in \mathrm{Unit}\left(Z\right)\right)$$
15	5	adantr	$$⊢\left(\phi \wedge a\in B\right)\to X\in D$$
16		simpr	$$⊢\left(\phi \wedge a\in B\right)\to a\in B$$
17	1 2 3 6 7 15 16	dchrn0	$$⊢\left(\phi \wedge a\in B\right)\to \left(X\left(a\right)\ne 0\leftrightarrow a\in \mathrm{Unit}\left(Z\right)\right)$$
18	17	biimpd	$$⊢\left(\phi \wedge a\in B\right)\to \left(X\left(a\right)\ne 0\to a\in \mathrm{Unit}\left(Z\right)\right)$$
19	18	necon1bd	$$⊢\left(\phi \wedge a\in B\right)\to \left(\neg a\in \mathrm{Unit}\left(Z\right)\to X\left(a\right)=0\right)$$
20	19	impr	$$⊢\left(\phi \wedge \left(a\in B\wedge \neg a\in \mathrm{Unit}\left(Z\right)\right)\right)\to X\left(a\right)=0$$
21	14 20	sylan2b	$$⊢\left(\phi \wedge a\in \left(B\setminus \mathrm{Unit}\left(Z\right)\right)\right)\to X\left(a\right)=0$$
22	1 3	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
23	2 6	znfi	$$⊢N\in \mathbb{N}\to B\in \mathrm{Fin}$$
24	5 22 23	3syl	$$⊢\phi \to B\in \mathrm{Fin}$$
25	9 13 21 24	fsumss	$$⊢\phi \to \sum _{a\in \mathrm{Unit}\left(Z\right)}X\left(a\right)=\sum _{a\in B}X\left(a\right)$$
26	1 2 3 4 5 7	dchrsum2	$$⊢\phi \to \sum _{a\in \mathrm{Unit}\left(Z\right)}X\left(a\right)=if\left(X=\underset{\dot{}}{1},\mathrm{\varphi }\left(N\right),0\right)$$
27	25 26	eqtr3d	$$⊢\phi \to \sum _{a\in B}X\left(a\right)=if\left(X=\underset{\dot{}}{1},\mathrm{\varphi }\left(N\right),0\right)$$