dchr2sum

Description: An orthogonality relation for Dirichlet characters: the sum of X ( a ) x. * Y ( a ) over all a is nonzero only when X = Y . Part of Theorem 6.5.2 of Shapiro p. 232. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchr2sum.g	$⊢ G = DChr (N)$
	dchr2sum.z	$⊢ Z = ℤ / N ℤ$
	dchr2sum.d	$⊢ D = {Base}_{G}$
	dchr2sum.b	$⊢ B = {Base}_{Z}$
	dchr2sum.x	$⊢ φ \to X \in D$
	dchr2sum.y	$⊢ φ \to Y \in D$
Assertion	dchr2sum	$⊢ φ \to \sum_{a \in B} X (a) \overline{Y (a)} = if (X = Y, ϕ (N), 0)$

Proof

Step	Hyp	Ref	Expression
1		dchr2sum.g	$⊢ G = DChr (N)$
2		dchr2sum.z	$⊢ Z = ℤ / N ℤ$
3		dchr2sum.d	$⊢ D = {Base}_{G}$
4		dchr2sum.b	$⊢ B = {Base}_{Z}$
5		dchr2sum.x	$⊢ φ \to X \in D$
6		dchr2sum.y	$⊢ φ \to Y \in D$
7		eqid	$⊢ 0_{G} = 0_{G}$
8	1 3	dchrrcl	$⊢ X \in D \to N \in ℕ$
9	5 8	syl	$⊢ φ \to N \in ℕ$
10	1	dchrabl	$⊢ N \in ℕ \to G \in Abel$
11		ablgrp	$⊢ G \in Abel \to G \in Grp$
12	9 10 11	3syl	$⊢ φ \to G \in Grp$
13		eqid	$⊢ -_{G} = -_{G}$
14	3 13	grpsubcl	$⊢ (G \in Grp \land X \in D \land Y \in D) \to X -_{G} Y \in D$
15	12 5 6 14	syl3anc	$⊢ φ \to X -_{G} Y \in D$
16	1 2 3 7 15 4	dchrsum	$⊢ φ \to \sum_{a \in B} (X -_{G} Y) (a) = if (X -_{G} Y = 0_{G}, ϕ (N), 0)$
17	5	adantr	$⊢ (φ \land a \in B) \to X \in D$
18	6	adantr	$⊢ (φ \land a \in B) \to Y \in D$
19		eqid	$⊢ +_{G} = +_{G}$
20		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
21	3 19 20 13	grpsubval	$⊢ (X \in D \land Y \in D) \to X -_{G} Y = X +_{G} {inv}_{g} (G) (Y)$
22	17 18 21	syl2anc	$⊢ (φ \land a \in B) \to X -_{G} Y = X +_{G} {inv}_{g} (G) (Y)$
23	9	adantr	$⊢ (φ \land a \in B) \to N \in ℕ$
24	23 10 11	3syl	$⊢ (φ \land a \in B) \to G \in Grp$
25	3 20	grpinvcl	$⊢ (G \in Grp \land Y \in D) \to {inv}_{g} (G) (Y) \in D$
26	24 18 25	syl2anc	$⊢ (φ \land a \in B) \to {inv}_{g} (G) (Y) \in D$
27	1 2 3 19 17 26	dchrmul	$⊢ (φ \land a \in B) \to X +_{G} {inv}_{g} (G) (Y) = X \times_{f} {inv}_{g} (G) (Y)$
28	22 27	eqtrd	$⊢ (φ \land a \in B) \to X -_{G} Y = X \times_{f} {inv}_{g} (G) (Y)$
29	28	fveq1d	$⊢ (φ \land a \in B) \to (X -_{G} Y) (a) = (X \times_{f} {inv}_{g} (G) (Y)) (a)$
30	1 2 3 4 17	dchrf	$⊢ (φ \land a \in B) \to X : B ⟶ ℂ$
31	30	ffnd	$⊢ (φ \land a \in B) \to X Fn B$
32	1 2 3 4 26	dchrf	$⊢ (φ \land a \in B) \to {inv}_{g} (G) (Y) : B ⟶ ℂ$
33	32	ffnd	$⊢ (φ \land a \in B) \to {inv}_{g} (G) (Y) Fn B$
34	4	fvexi	$⊢ B \in V$
35	34	a1i	$⊢ (φ \land a \in B) \to B \in V$
36		simpr	$⊢ (φ \land a \in B) \to a \in B$
37		fnfvof	$⊢ ((X Fn B \land {inv}_{g} (G) (Y) Fn B) \land (B \in V \land a \in B)) \to (X \times_{f} {inv}_{g} (G) (Y)) (a) = X (a) {inv}_{g} (G) (Y) (a)$
38	31 33 35 36 37	syl22anc	$⊢ (φ \land a \in B) \to (X \times_{f} {inv}_{g} (G) (Y)) (a) = X (a) {inv}_{g} (G) (Y) (a)$
39	1 3 18 20	dchrinv	$⊢ (φ \land a \in B) \to {inv}_{g} (G) (Y) = * \circ Y$
40	39	fveq1d	$⊢ (φ \land a \in B) \to {inv}_{g} (G) (Y) (a) = (* \circ Y) (a)$
41	1 2 3 4 18	dchrf	$⊢ (φ \land a \in B) \to Y : B ⟶ ℂ$
42		fvco3	$⊢ (Y : B ⟶ ℂ \land a \in B) \to (* \circ Y) (a) = \overline{Y (a)}$
43	41 36 42	syl2anc	$⊢ (φ \land a \in B) \to (* \circ Y) (a) = \overline{Y (a)}$
44	40 43	eqtrd	$⊢ (φ \land a \in B) \to {inv}_{g} (G) (Y) (a) = \overline{Y (a)}$
45	44	oveq2d	$⊢ (φ \land a \in B) \to X (a) {inv}_{g} (G) (Y) (a) = X (a) \overline{Y (a)}$
46	29 38 45	3eqtrd	$⊢ (φ \land a \in B) \to (X -_{G} Y) (a) = X (a) \overline{Y (a)}$
47	46	sumeq2dv	$⊢ φ \to \sum_{a \in B} (X -_{G} Y) (a) = \sum_{a \in B} X (a) \overline{Y (a)}$
48	3 7 13	grpsubeq0	$⊢ (G \in Grp \land X \in D \land Y \in D) \to (X -_{G} Y = 0_{G} \leftrightarrow X = Y)$
49	12 5 6 48	syl3anc	$⊢ φ \to (X -_{G} Y = 0_{G} \leftrightarrow X = Y)$
50	49	ifbid	$⊢ φ \to if (X -_{G} Y = 0_{G}, ϕ (N), 0) = if (X = Y, ϕ (N), 0)$
51	16 47 50	3eqtr3d	$⊢ φ \to \sum_{a \in B} X (a) \overline{Y (a)} = if (X = Y, ϕ (N), 0)$

Metamath Proof Explorer

Theorem dchr2sum

Proof