Theorem sum2dchr

Description: An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Part of Theorem 6.5.2 of Shapiro p. 232. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	sum2dchr.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	sum2dchr.d	$$⊢D={\mathrm{Base}}_G$$
	sum2dchr.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	sum2dchr.b	$$⊢B={\mathrm{Base}}_Z$$
	sum2dchr.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	sum2dchr.n	$$⊢\phi \to N\in \mathbb{N}$$
	sum2dchr.a	$$⊢\phi \to A\in B$$
	sum2dchr.c	$$⊢\phi \to C\in U$$
Assertion	sum2dchr	$$⊢\phi \to \sum _{x\in D}x\left(A\right)\overline{x\left(C\right)}=if\left(A=C,\mathrm{\varphi }\left(N\right),0\right)$$

Proof

Step	Hyp	Ref	Expression
1		sum2dchr.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		sum2dchr.d	$$⊢D={\mathrm{Base}}_G$$
3		sum2dchr.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
4		sum2dchr.b	$$⊢B={\mathrm{Base}}_Z$$
5		sum2dchr.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
6		sum2dchr.n	$$⊢\phi \to N\in \mathbb{N}$$
7		sum2dchr.a	$$⊢\phi \to A\in B$$
8		sum2dchr.c	$$⊢\phi \to C\in U$$
9		eqid	$$⊢1_Z=1_Z$$
10	6	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11	3	zncrng	$$⊢N\in {\mathbb{N}}_0\to Z\in \mathrm{CRing}$$
12		crngring	$$⊢Z\in \mathrm{CRing}\to Z\in \mathrm{Ring}$$
13	10 11 12	3syl	$$⊢\phi \to Z\in \mathrm{Ring}$$
14		eqid	$$⊢{/}_r\left(Z\right)={/}_r\left(Z\right)$$
15	4 5 14	dvrcl	$$⊢\left(Z\in \mathrm{Ring}\wedge A\in B\wedge C\in U\right)\to A{/}_r\left(Z\right)C\in B$$
16	13 7 8 15	syl3anc	$$⊢\phi \to A{/}_r\left(Z\right)C\in B$$
17	1 2 3 9 4 6 16	sumdchr	$$⊢\phi \to \sum _{x\in D}x\left(A{/}_r\left(Z\right)C\right)=if\left(A{/}_r\left(Z\right)C=1_Z,\mathrm{\varphi }\left(N\right),0\right)$$
18		eqid	$$⊢{\cdot }_Z={\cdot }_Z$$
19		eqid	$$⊢{inv}_r\left(Z\right)={inv}_r\left(Z\right)$$
20	4 18 5 19 14	dvrval	$$⊢\left(A\in B\wedge C\in U\right)\to A{/}_r\left(Z\right)C=A{\cdot }_Z{inv}_r\left(Z\right)\left(C\right)$$
21	7 8 20	syl2anc	$$⊢\phi \to A{/}_r\left(Z\right)C=A{\cdot }_Z{inv}_r\left(Z\right)\left(C\right)$$
22	21	adantr	$$⊢\left(\phi \wedge x\in D\right)\to A{/}_r\left(Z\right)C=A{\cdot }_Z{inv}_r\left(Z\right)\left(C\right)$$
23	22	fveq2d	$$⊢\left(\phi \wedge x\in D\right)\to x\left(A{/}_r\left(Z\right)C\right)=x\left(A{\cdot }_Z{inv}_r\left(Z\right)\left(C\right)\right)$$
24	1 3 2	dchrmhm	$$⊢D\subseteq {\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
25		simpr	$$⊢\left(\phi \wedge x\in D\right)\to x\in D$$
26	24 25	sselid	$$⊢\left(\phi \wedge x\in D\right)\to x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
27	7	adantr	$$⊢\left(\phi \wedge x\in D\right)\to A\in B$$
28	4 5	unitss	$$⊢U\subseteq B$$
29	5 19	unitinvcl	$$⊢\left(Z\in \mathrm{Ring}\wedge C\in U\right)\to {inv}_r\left(Z\right)\left(C\right)\in U$$
30	13 8 29	syl2anc	$$⊢\phi \to {inv}_r\left(Z\right)\left(C\right)\in U$$
31	30	adantr	$$⊢\left(\phi \wedge x\in D\right)\to {inv}_r\left(Z\right)\left(C\right)\in U$$
32	28 31	sselid	$$⊢\left(\phi \wedge x\in D\right)\to {inv}_r\left(Z\right)\left(C\right)\in B$$
33		eqid	$$⊢{\mathrm{mulGrp}}_Z={\mathrm{mulGrp}}_Z$$
34	33 4	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_Z}$$
35	33 18	mgpplusg	$$⊢{\cdot }_Z={+}_{{\mathrm{mulGrp}}_Z}$$
36		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
37		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
38	36 37	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
39	34 35 38	mhmlin	$$⊢\left(x\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge A\in B\wedge {inv}_r\left(Z\right)\left(C\right)\in B\right)\to x\left(A{\cdot }_Z{inv}_r\left(Z\right)\left(C\right)\right)=x\left(A\right)x\left({inv}_r\left(Z\right)\left(C\right)\right)$$
40	26 27 32 39	syl3anc	$$⊢\left(\phi \wedge x\in D\right)\to x\left(A{\cdot }_Z{inv}_r\left(Z\right)\left(C\right)\right)=x\left(A\right)x\left({inv}_r\left(Z\right)\left(C\right)\right)$$
41		eqid	$$⊢{\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U={\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U$$
42		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
43	1 3 2 5 41 42 25	dchrghm	$$⊢\left(\phi \wedge x\in D\right)\to {x\upharpoonright }_U\in \left(\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)$$
44	8	adantr	$$⊢\left(\phi \wedge x\in D\right)\to C\in U$$
45	5 41	unitgrpbas	$$⊢U={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}$$
46	5 41 19	invrfval	$$⊢{inv}_r\left(Z\right)={inv}_g\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)$$
47		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
48		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
49		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
50	47 48 49	drngui	$$⊢ℂ\setminus \left\{0\right\}=\mathrm{Unit}\left({ℂ}_{\mathrm{fld}}\right)$$
51		eqid	$$⊢{inv}_r\left({ℂ}_{\mathrm{fld}}\right)={inv}_r\left({ℂ}_{\mathrm{fld}}\right)$$
52	50 42 51	invrfval	$$⊢{inv}_r\left({ℂ}_{\mathrm{fld}}\right)={inv}_g\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
53	45 46 52	ghminv	$$⊢\left({x\upharpoonright }_U\in \left(\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)\mathrm{GrpHom}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\right)\wedge C\in U\right)\to \left({x\upharpoonright }_U\right)\left({inv}_r\left(Z\right)\left(C\right)\right)={inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(\left({x\upharpoonright }_U\right)\left(C\right)\right)$$
54	43 44 53	syl2anc	$$⊢\left(\phi \wedge x\in D\right)\to \left({x\upharpoonright }_U\right)\left({inv}_r\left(Z\right)\left(C\right)\right)={inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(\left({x\upharpoonright }_U\right)\left(C\right)\right)$$
55	31	fvresd	$$⊢\left(\phi \wedge x\in D\right)\to \left({x\upharpoonright }_U\right)\left({inv}_r\left(Z\right)\left(C\right)\right)=x\left({inv}_r\left(Z\right)\left(C\right)\right)$$
56	44	fvresd	$$⊢\left(\phi \wedge x\in D\right)\to \left({x\upharpoonright }_U\right)\left(C\right)=x\left(C\right)$$
57	56	fveq2d	$$⊢\left(\phi \wedge x\in D\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(\left({x\upharpoonright }_U\right)\left(C\right)\right)={inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\left(C\right)\right)$$
58	1 3 2 4 25	dchrf	$$⊢\left(\phi \wedge x\in D\right)\to x:B⟶ℂ$$
59	28 44	sselid	$$⊢\left(\phi \wedge x\in D\right)\to C\in B$$
60	58 59	ffvelcdmd	$$⊢\left(\phi \wedge x\in D\right)\to x\left(C\right)\in ℂ$$
61	1 3 2 4 5 25 59	dchrn0	$$⊢\left(\phi \wedge x\in D\right)\to \left(x\left(C\right)\ne 0\leftrightarrow C\in U\right)$$
62	44 61	mpbird	$$⊢\left(\phi \wedge x\in D\right)\to x\left(C\right)\ne 0$$
63		cnfldinv	$$⊢\left(x\left(C\right)\in ℂ\wedge x\left(C\right)\ne 0\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\left(C\right)\right)=\frac{1}{x\left(C\right)}$$
64	60 62 63	syl2anc	$$⊢\left(\phi \wedge x\in D\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\left(C\right)\right)=\frac{1}{x\left(C\right)}$$
65		recval	$$⊢\left(x\left(C\right)\in ℂ\wedge x\left(C\right)\ne 0\right)\to \frac{1}{x\left(C\right)}=\frac{\overline{x\left(C\right)}}{{\left|x\left(C\right)\right|}^2}$$
66	60 62 65	syl2anc	$$⊢\left(\phi \wedge x\in D\right)\to \frac{1}{x\left(C\right)}=\frac{\overline{x\left(C\right)}}{{\left|x\left(C\right)\right|}^2}$$
67	1 2 25 3 5 44	dchrabs	$$⊢\left(\phi \wedge x\in D\right)\to \left|x\left(C\right)\right|=1$$
68	67	oveq1d	$$⊢\left(\phi \wedge x\in D\right)\to {\left|x\left(C\right)\right|}^2=1^2$$
69		sq1	$$⊢1^2=1$$
70	68 69	eqtrdi	$$⊢\left(\phi \wedge x\in D\right)\to {\left|x\left(C\right)\right|}^2=1$$
71	70	oveq2d	$$⊢\left(\phi \wedge x\in D\right)\to \frac{\overline{x\left(C\right)}}{{\left|x\left(C\right)\right|}^2}=\frac{\overline{x\left(C\right)}}{1}$$
72	60	cjcld	$$⊢\left(\phi \wedge x\in D\right)\to \overline{x\left(C\right)}\in ℂ$$
73	72	div1d	$$⊢\left(\phi \wedge x\in D\right)\to \frac{\overline{x\left(C\right)}}{1}=\overline{x\left(C\right)}$$
74	66 71 73	3eqtrd	$$⊢\left(\phi \wedge x\in D\right)\to \frac{1}{x\left(C\right)}=\overline{x\left(C\right)}$$
75	57 64 74	3eqtrd	$$⊢\left(\phi \wedge x\in D\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(\left({x\upharpoonright }_U\right)\left(C\right)\right)=\overline{x\left(C\right)}$$
76	54 55 75	3eqtr3d	$$⊢\left(\phi \wedge x\in D\right)\to x\left({inv}_r\left(Z\right)\left(C\right)\right)=\overline{x\left(C\right)}$$
77	76	oveq2d	$$⊢\left(\phi \wedge x\in D\right)\to x\left(A\right)x\left({inv}_r\left(Z\right)\left(C\right)\right)=x\left(A\right)\overline{x\left(C\right)}$$
78	23 40 77	3eqtrd	$$⊢\left(\phi \wedge x\in D\right)\to x\left(A{/}_r\left(Z\right)C\right)=x\left(A\right)\overline{x\left(C\right)}$$
79	78	sumeq2dv	$$⊢\phi \to \sum _{x\in D}x\left(A{/}_r\left(Z\right)C\right)=\sum _{x\in D}x\left(A\right)\overline{x\left(C\right)}$$
80	4 5 14 9	dvreq1	$$⊢\left(Z\in \mathrm{Ring}\wedge A\in B\wedge C\in U\right)\to \left(A{/}_r\left(Z\right)C=1_Z\leftrightarrow A=C\right)$$
81	13 7 8 80	syl3anc	$$⊢\phi \to \left(A{/}_r\left(Z\right)C=1_Z\leftrightarrow A=C\right)$$
82	81	ifbid	$$⊢\phi \to if\left(A{/}_r\left(Z\right)C=1_Z,\mathrm{\varphi }\left(N\right),0\right)=if\left(A=C,\mathrm{\varphi }\left(N\right),0\right)$$
83	17 79 82	3eqtr3d	$$⊢\phi \to \sum _{x\in D}x\left(A\right)\overline{x\left(C\right)}=if\left(A=C,\mathrm{\varphi }\left(N\right),0\right)$$