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	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	sum2dchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	sum2dchr.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	sum2dchr.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	sum2dchr.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	sum2dchr.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	sum2dchr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	sum2dchr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
Assertion	sum2dchr	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		sum2dchr.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		sum2dchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
3		sum2dchr.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
4		sum2dchr.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
5		sum2dchr.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
6		sum2dchr.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		sum2dchr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8		sum2dchr.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
9		eqid	⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
10	6	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11	3	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
12		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
13	10 11 12	3syl	⊢ ( 𝜑 → 𝑍 ∈ Ring )
14		eqid	⊢ ( /r ‘ 𝑍 ) = ( /r ‘ 𝑍 )
15	4 5 14	dvrcl	⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ∈ 𝐵 )
16	13 7 8 15	syl3anc	⊢ ( 𝜑 → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ∈ 𝐵 )
17	1 2 3 9 4 6 16	sumdchr	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = if ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) , ( ϕ ‘ 𝑁 ) , 0 ) )
18		eqid	⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
19		eqid	⊢ ( invr ‘ 𝑍 ) = ( invr ‘ 𝑍 )
20	4 18 5 19 14	dvrval	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
21	7 8 20	syl2anc	⊢ ( 𝜑 → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
23	22	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) )
24	1 3 2	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
26	24 25	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
27	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝐵 )
28	4 5	unitss	⊢ 𝑈 ⊆ 𝐵
29	5 19	unitinvcl	⊢ ( ( 𝑍 ∈ Ring ∧ 𝐶 ∈ 𝑈 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 )
30	13 8 29	syl2anc	⊢ ( 𝜑 → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 )
32	28 31	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝐵 )
33		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
34	33 4	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
35	33 18	mgpplusg	⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
36		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
37		cnfldmul	⊢ · = ( .r ‘ ℂfld )
38	36 37	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
39	34 35 38	mhmlin	⊢ ( ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝐴 ∈ 𝐵 ∧ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) )
40	26 27 32 39	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) )
41		eqid	⊢ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
42		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
43	1 3 2 5 41 42 25	dchrghm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) )
44	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐶 ∈ 𝑈 )
45	5 41	unitgrpbas	⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
46	5 41 19	invrfval	⊢ ( invr ‘ 𝑍 ) = ( invg ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
47		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
48		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
49		cndrng	⊢ ℂfld ∈ DivRing
50	47 48 49	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
51		eqid	⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
52	50 42 51	invrfval	⊢ ( invr ‘ ℂfld ) = ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
53	45 46 52	ghminv	⊢ ( ( ( 𝑥 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) )
54	43 44 53	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) )
55	31	fvresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) )
56	44	fvresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) = ( 𝑥 ‘ 𝐶 ) )
57	56	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) )
58	1 3 2 4 25	dchrf	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐵 ⟶ ℂ )
59	28 44	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐶 ∈ 𝐵 )
60	58 59	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐶 ) ∈ ℂ )
61	1 3 2 4 5 25 59	dchrn0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ‘ 𝐶 ) ≠ 0 ↔ 𝐶 ∈ 𝑈 ) )
62	44 61	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐶 ) ≠ 0 )
63		cnfldinv	⊢ ( ( ( 𝑥 ‘ 𝐶 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝐶 ) ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) = ( 1 / ( 𝑥 ‘ 𝐶 ) ) )
64	60 62 63	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) = ( 1 / ( 𝑥 ‘ 𝐶 ) ) )
65		recval	⊢ ( ( ( 𝑥 ‘ 𝐶 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝐶 ) ≠ 0 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) )
66	60 62 65	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) )
67	1 2 25 3 5 44	dchrabs	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) = 1 )
68	67	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
69		sq1	⊢ ( 1 ↑ 2 ) = 1
70	68 69	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) = 1 )
71	70	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / 1 ) )
72	60	cjcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ∈ ℂ )
73	72	div1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / 1 ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
74	66 71 73	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
75	57 64 74	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
76	54 55 75	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) )
77	76	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) )
78	23 40 77	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) )
79	78	sumeq2dv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) )
80	4 5 14 9	dvreq1	⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) ↔ 𝐴 = 𝐶 ) )
81	13 7 8 80	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) ↔ 𝐴 = 𝐶 ) )
82	81	ifbid	⊢ ( 𝜑 → if ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) , ( ϕ ‘ 𝑁 ) , 0 ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) )
83	17 79 82	3eqtr3d	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) )