dchrsum2

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 = DChr (N)$
	dchrsum.z	$⊢ Z = ℤ / N ℤ$
	dchrsum.d	$⊢ D = {Base}_{G}$
	dchrsum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrsum.x	$⊢ φ \to X \in D$
	dchrsum2.u	$⊢ U = Unit (Z)$
Assertion	dchrsum2	$⊢ φ \to \sum_{a \in U} X (a) = if (X = \underset{˙}{1}, ϕ (N), 0)$

Proof

Step	Hyp	Ref	Expression
1		dchrsum.g	$⊢ G = DChr (N)$
2		dchrsum.z	$⊢ Z = ℤ / N ℤ$
3		dchrsum.d	$⊢ D = {Base}_{G}$
4		dchrsum.1	$⊢ \underset{˙}{1} = 0_{G}$
5		dchrsum.x	$⊢ φ \to X \in D$
6		dchrsum2.u	$⊢ U = Unit (Z)$
7		eqeq2	$⊢ ϕ (N) = if (X = \underset{˙}{1}, ϕ (N), 0) \to (\sum_{a \in U} X (a) = ϕ (N) \leftrightarrow \sum_{a \in U} X (a) = if (X = \underset{˙}{1}, ϕ (N), 0))$
8		eqeq2	$⊢ 0 = if (X = \underset{˙}{1}, ϕ (N), 0) \to (\sum_{a \in U} X (a) = 0 \leftrightarrow \sum_{a \in U} X (a) = if (X = \underset{˙}{1}, ϕ (N), 0))$
9		fveq1	$⊢ X = \underset{˙}{1} \to X (a) = \underset{˙}{1} (a)$
10	1 3	dchrrcl	$⊢ X \in D \to N \in ℕ$
11	5 10	syl	$⊢ φ \to N \in ℕ$
12	11	adantr	$⊢ (φ \land a \in U) \to N \in ℕ$
13		simpr	$⊢ (φ \land a \in U) \to a \in U$
14	1 2 4 6 12 13	dchr1	$⊢ (φ \land a \in U) \to \underset{˙}{1} (a) = 1$
15	9 14	sylan9eqr	$⊢ ((φ \land a \in U) \land X = \underset{˙}{1}) \to X (a) = 1$
16	15	an32s	$⊢ ((φ \land X = \underset{˙}{1}) \land a \in U) \to X (a) = 1$
17	16	sumeq2dv	$⊢ (φ \land X = \underset{˙}{1}) \to \sum_{a \in U} X (a) = \sum_{a \in U} 1$
18	2 6	znunithash	$⊢ N \in ℕ \to \|U\| = ϕ (N)$
19	11 18	syl	$⊢ φ \to \|U\| = ϕ (N)$
20	11	phicld	$⊢ φ \to ϕ (N) \in ℕ$
21	20	nnnn0d	$⊢ φ \to ϕ (N) \in ℕ_{0}$
22	19 21	eqeltrd	$⊢ φ \to \|U\| \in ℕ_{0}$
23	6	fvexi	$⊢ U \in V$
24		hashclb	$⊢ U \in V \to (U \in Fin \leftrightarrow \|U\| \in ℕ_{0})$
25	23 24	ax-mp	$⊢ U \in Fin \leftrightarrow \|U\| \in ℕ_{0}$
26	22 25	sylibr	$⊢ φ \to U \in Fin$
27		ax-1cn	$⊢ 1 \in ℂ$
28		fsumconst	$⊢ (U \in Fin \land 1 \in ℂ) \to \sum_{a \in U} 1 = \|U\| \cdot 1$
29	26 27 28	sylancl	$⊢ φ \to \sum_{a \in U} 1 = \|U\| \cdot 1$
30	19	oveq1d	$⊢ φ \to \|U\| \cdot 1 = ϕ (N) \cdot 1$
31	20	nncnd	$⊢ φ \to ϕ (N) \in ℂ$
32	31	mulid1d	$⊢ φ \to ϕ (N) \cdot 1 = ϕ (N)$
33	29 30 32	3eqtrd	$⊢ φ \to \sum_{a \in U} 1 = ϕ (N)$
34	33	adantr	$⊢ (φ \land X = \underset{˙}{1}) \to \sum_{a \in U} 1 = ϕ (N)$
35	17 34	eqtrd	$⊢ (φ \land X = \underset{˙}{1}) \to \sum_{a \in U} X (a) = ϕ (N)$
36	1	dchrabl	$⊢ N \in ℕ \to G \in Abel$
37		ablgrp	$⊢ G \in Abel \to G \in Grp$
38	3 4	grpidcl	$⊢ G \in Grp \to \underset{˙}{1} \in D$
39	11 36 37 38	4syl	$⊢ φ \to \underset{˙}{1} \in D$
40	1 2 3 6 5 39	dchreq	$⊢ φ \to (X = \underset{˙}{1} \leftrightarrow \forall k \in U X (k) = \underset{˙}{1} (k))$
41	40	notbid	$⊢ φ \to (\neg X = \underset{˙}{1} \leftrightarrow \neg \forall k \in U X (k) = \underset{˙}{1} (k))$
42		rexnal	$⊢ \exists k \in U \neg X (k) = \underset{˙}{1} (k) \leftrightarrow \neg \forall k \in U X (k) = \underset{˙}{1} (k)$
43	41 42	bitr4di	$⊢ φ \to (\neg X = \underset{˙}{1} \leftrightarrow \exists k \in U \neg X (k) = \underset{˙}{1} (k))$
44		df-ne	$⊢ X (k) \neq \underset{˙}{1} (k) \leftrightarrow \neg X (k) = \underset{˙}{1} (k)$
45	11	adantr	$⊢ (φ \land k \in U) \to N \in ℕ$
46		simpr	$⊢ (φ \land k \in U) \to k \in U$
47	1 2 4 6 45 46	dchr1	$⊢ (φ \land k \in U) \to \underset{˙}{1} (k) = 1$
48	47	neeq2d	$⊢ (φ \land k \in U) \to (X (k) \neq \underset{˙}{1} (k) \leftrightarrow X (k) \neq 1)$
49	26	adantr	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to U \in Fin$
50		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
51	1 2 3 50 5	dchrf	$⊢ φ \to X : {Base}_{Z} ⟶ ℂ$
52	50 6	unitss	$⊢ U \subseteq {Base}_{Z}$
53	52	sseli	$⊢ a \in U \to a \in {Base}_{Z}$
54		ffvelrn	$⊢ (X : {Base}_{Z} ⟶ ℂ \land a \in {Base}_{Z}) \to X (a) \in ℂ$
55	51 53 54	syl2an	$⊢ (φ \land a \in U) \to X (a) \in ℂ$
56	55	adantlr	$⊢ ((φ \land (k \in U \land X (k) \neq 1)) \land a \in U) \to X (a) \in ℂ$
57	49 56	fsumcl	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to \sum_{a \in U} X (a) \in ℂ$
58		0cnd	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to 0 \in ℂ$
59	51	adantr	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X : {Base}_{Z} ⟶ ℂ$
60		simprl	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to k \in U$
61	52 60	sselid	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to k \in {Base}_{Z}$
62	59 61	ffvelrnd	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) \in ℂ$
63		subcl	$⊢ (X (k) \in ℂ \land 1 \in ℂ) \to X (k) - 1 \in ℂ$
64	62 27 63	sylancl	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) - 1 \in ℂ$
65		simprr	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) \neq 1$
66		subeq0	$⊢ (X (k) \in ℂ \land 1 \in ℂ) \to (X (k) - 1 = 0 \leftrightarrow X (k) = 1)$
67	62 27 66	sylancl	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to (X (k) - 1 = 0 \leftrightarrow X (k) = 1)$
68	67	necon3bid	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to (X (k) - 1 \neq 0 \leftrightarrow X (k) \neq 1)$
69	65 68	mpbird	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) - 1 \neq 0$
70		oveq2	$⊢ x = a \to k \cdot_{Z} x = k \cdot_{Z} a$
71	70	fveq2d	$⊢ x = a \to X (k \cdot_{Z} x) = X (k \cdot_{Z} a)$
72	71	cbvsumv	$⊢ \sum_{x \in U} X (k \cdot_{Z} x) = \sum_{a \in U} X (k \cdot_{Z} a)$
73	1 2 3	dchrmhm	$⊢ D \subseteq {mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}$
74	73 5	sselid	$⊢ φ \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
75	74	ad2antrr	$⊢ ((φ \land (k \in U \land X (k) \neq 1)) \land a \in U) \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
76	61	adantr	$⊢ ((φ \land (k \in U \land X (k) \neq 1)) \land a \in U) \to k \in {Base}_{Z}$
77	53	adantl	$⊢ ((φ \land (k \in U \land X (k) \neq 1)) \land a \in U) \to a \in {Base}_{Z}$
78		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
79	78 50	mgpbas	$⊢ {Base}_{Z} = {Base}_{{mulGrp}_{Z}}$
80		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
81	78 80	mgpplusg	$⊢ \cdot_{Z} = +_{{mulGrp}_{Z}}$
82		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
83		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
84	82 83	mgpplusg	$⊢ \times = +_{{mulGrp}_{ℂ_{fld}}}$
85	79 81 84	mhmlin	$⊢ (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land k \in {Base}_{Z} \land a \in {Base}_{Z}) \to X (k \cdot_{Z} a) = X (k) X (a)$
86	75 76 77 85	syl3anc	$⊢ ((φ \land (k \in U \land X (k) \neq 1)) \land a \in U) \to X (k \cdot_{Z} a) = X (k) X (a)$
87	86	sumeq2dv	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to \sum_{a \in U} X (k \cdot_{Z} a) = \sum_{a \in U} X (k) X (a)$
88	72 87	syl5eq	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to \sum_{x \in U} X (k \cdot_{Z} x) = \sum_{a \in U} X (k) X (a)$
89		fveq2	$⊢ a = k \cdot_{Z} x \to X (a) = X (k \cdot_{Z} x)$
90	11	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
91	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
92		crngring	$⊢ Z \in CRing \to Z \in Ring$
93		eqid	$⊢ {mulGrp}_{Z} ↾_{𝑠} U = {mulGrp}_{Z} ↾_{𝑠} U$
94	6 93	unitgrp	$⊢ Z \in Ring \to {mulGrp}_{Z} ↾_{𝑠} U \in Grp$
95	90 91 92 94	4syl	$⊢ φ \to {mulGrp}_{Z} ↾_{𝑠} U \in Grp$
96		eqid	$⊢ (b \in U ⟼ (c \in U ⟼ b \cdot_{Z} c)) = (b \in U ⟼ (c \in U ⟼ b \cdot_{Z} c))$
97	6 93	unitgrpbas	$⊢ U = {Base}_{({mulGrp}_{Z} ↾_{𝑠} U)}$
98	93 81	ressplusg	$⊢ U \in V \to \cdot_{Z} = +_{({mulGrp}_{Z} ↾_{𝑠} U)}$
99	23 98	ax-mp	$⊢ \cdot_{Z} = +_{({mulGrp}_{Z} ↾_{𝑠} U)}$
100	96 97 99	grplactf1o	$⊢ ({mulGrp}_{Z} ↾_{𝑠} U \in Grp \land k \in U) \to (b \in U ⟼ (c \in U ⟼ b \cdot_{Z} c)) (k) : U \underset{1-1 onto}{⟶} U$
101	95 60 100	syl2an2r	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to (b \in U ⟼ (c \in U ⟼ b \cdot_{Z} c)) (k) : U \underset{1-1 onto}{⟶} U$
102	96 97	grplactval	$⊢ (k \in U \land x \in U) \to (b \in U ⟼ (c \in U ⟼ b \cdot_{Z} c)) (k) (x) = k \cdot_{Z} x$
103	60 102	sylan	$⊢ ((φ \land (k \in U \land X (k) \neq 1)) \land x \in U) \to (b \in U ⟼ (c \in U ⟼ b \cdot_{Z} c)) (k) (x) = k \cdot_{Z} x$
104	89 49 101 103 56	fsumf1o	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to \sum_{a \in U} X (a) = \sum_{x \in U} X (k \cdot_{Z} x)$
105	49 62 56	fsummulc2	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) \sum_{a \in U} X (a) = \sum_{a \in U} X (k) X (a)$
106	88 104 105	3eqtr4rd	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) \sum_{a \in U} X (a) = \sum_{a \in U} X (a)$
107	57	mulid2d	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to 1 \sum_{a \in U} X (a) = \sum_{a \in U} X (a)$
108	106 107	oveq12d	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) \sum_{a \in U} X (a) - 1 \sum_{a \in U} X (a) = \sum_{a \in U} X (a) - \sum_{a \in U} X (a)$
109	57	subidd	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to \sum_{a \in U} X (a) - \sum_{a \in U} X (a) = 0$
110	108 109	eqtrd	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to X (k) \sum_{a \in U} X (a) - 1 \sum_{a \in U} X (a) = 0$
111		1cnd	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to 1 \in ℂ$
112	62 111 57	subdird	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to (X (k) - 1) \sum_{a \in U} X (a) = X (k) \sum_{a \in U} X (a) - 1 \sum_{a \in U} X (a)$
113	64	mul01d	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to (X (k) - 1) \cdot 0 = 0$
114	110 112 113	3eqtr4d	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to (X (k) - 1) \sum_{a \in U} X (a) = (X (k) - 1) \cdot 0$
115	57 58 64 69 114	mulcanad	$⊢ (φ \land (k \in U \land X (k) \neq 1)) \to \sum_{a \in U} X (a) = 0$
116	115	expr	$⊢ (φ \land k \in U) \to (X (k) \neq 1 \to \sum_{a \in U} X (a) = 0)$
117	48 116	sylbid	$⊢ (φ \land k \in U) \to (X (k) \neq \underset{˙}{1} (k) \to \sum_{a \in U} X (a) = 0)$
118	44 117	syl5bir	$⊢ (φ \land k \in U) \to (\neg X (k) = \underset{˙}{1} (k) \to \sum_{a \in U} X (a) = 0)$
119	118	rexlimdva	$⊢ φ \to (\exists k \in U \neg X (k) = \underset{˙}{1} (k) \to \sum_{a \in U} X (a) = 0)$
120	43 119	sylbid	$⊢ φ \to (\neg X = \underset{˙}{1} \to \sum_{a \in U} X (a) = 0)$
121	120	imp	$⊢ (φ \land \neg X = \underset{˙}{1}) \to \sum_{a \in U} X (a) = 0$
122	7 8 35 121	ifbothda	$⊢ φ \to \sum_{a \in U} X (a) = if (X = \underset{˙}{1}, ϕ (N), 0)$

Metamath Proof Explorer

Theorem dchrsum2

Proof