dchrhash

Description: There are exactly phi ( N ) Dirichlet characters modulo N . Part of Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	sumdchr.g	$⊢ G = DChr (N)$
	sumdchr.d	$⊢ D = {Base}_{G}$
Assertion	dchrhash	$⊢ N \in ℕ \to \|D\| = ϕ (N)$

Proof

Step	Hyp	Ref	Expression
1		sumdchr.g	$⊢ G = DChr (N)$
2		sumdchr.d	$⊢ D = {Base}_{G}$
3		eqid	$⊢ ℤ / N ℤ = ℤ / N ℤ$
4		eqid	$⊢ {Base}_{ℤ / N ℤ} = {Base}_{ℤ / N ℤ}$
5	3 4	znfi	$⊢ N \in ℕ \to {Base}_{ℤ / N ℤ} \in Fin$
6	1 2	dchrfi	$⊢ N \in ℕ \to D \in Fin$
7		simprr	$⊢ (N \in ℕ \land (a \in {Base}_{ℤ / N ℤ} \land x \in D)) \to x \in D$
8	1 3 2 4 7	dchrf	$⊢ (N \in ℕ \land (a \in {Base}_{ℤ / N ℤ} \land x \in D)) \to x : {Base}_{ℤ / N ℤ} ⟶ ℂ$
9		simprl	$⊢ (N \in ℕ \land (a \in {Base}_{ℤ / N ℤ} \land x \in D)) \to a \in {Base}_{ℤ / N ℤ}$
10	8 9	ffvelrnd	$⊢ (N \in ℕ \land (a \in {Base}_{ℤ / N ℤ} \land x \in D)) \to x (a) \in ℂ$
11	5 6 10	fsumcom	$⊢ N \in ℕ \to \sum_{a \in {Base}_{ℤ / N ℤ}} \sum_{x \in D} x (a) = \sum_{x \in D} \sum_{a \in {Base}_{ℤ / N ℤ}} x (a)$
12		eqid	$⊢ 1_{ℤ / N ℤ} = 1_{ℤ / N ℤ}$
13		simpl	$⊢ (N \in ℕ \land a \in {Base}_{ℤ / N ℤ}) \to N \in ℕ$
14		simpr	$⊢ (N \in ℕ \land a \in {Base}_{ℤ / N ℤ}) \to a \in {Base}_{ℤ / N ℤ}$
15	1 2 3 12 4 13 14	sumdchr2	$⊢ (N \in ℕ \land a \in {Base}_{ℤ / N ℤ}) \to \sum_{x \in D} x (a) = if (a = 1_{ℤ / N ℤ}, \|D\|, 0)$
16		velsn	$⊢ a \in \{1_{ℤ / N ℤ}\} \leftrightarrow a = 1_{ℤ / N ℤ}$
17		ifbi	$⊢ (a \in \{1_{ℤ / N ℤ}\} \leftrightarrow a = 1_{ℤ / N ℤ}) \to if (a \in \{1_{ℤ / N ℤ}\}, \|D\|, 0) = if (a = 1_{ℤ / N ℤ}, \|D\|, 0)$
18	16 17	mp1i	$⊢ (N \in ℕ \land a \in {Base}_{ℤ / N ℤ}) \to if (a \in \{1_{ℤ / N ℤ}\}, \|D\|, 0) = if (a = 1_{ℤ / N ℤ}, \|D\|, 0)$
19	15 18	eqtr4d	$⊢ (N \in ℕ \land a \in {Base}_{ℤ / N ℤ}) \to \sum_{x \in D} x (a) = if (a \in \{1_{ℤ / N ℤ}\}, \|D\|, 0)$
20	19	sumeq2dv	$⊢ N \in ℕ \to \sum_{a \in {Base}_{ℤ / N ℤ}} \sum_{x \in D} x (a) = \sum_{a \in {Base}_{ℤ / N ℤ}} if (a \in \{1_{ℤ / N ℤ}\}, \|D\|, 0)$
21		eqid	$⊢ 0_{G} = 0_{G}$
22		simpr	$⊢ (N \in ℕ \land x \in D) \to x \in D$
23	1 3 2 21 22 4	dchrsum	$⊢ (N \in ℕ \land x \in D) \to \sum_{a \in {Base}_{ℤ / N ℤ}} x (a) = if (x = 0_{G}, ϕ (N), 0)$
24		velsn	$⊢ x \in \{0_{G}\} \leftrightarrow x = 0_{G}$
25		ifbi	$⊢ (x \in \{0_{G}\} \leftrightarrow x = 0_{G}) \to if (x \in \{0_{G}\}, ϕ (N), 0) = if (x = 0_{G}, ϕ (N), 0)$
26	24 25	mp1i	$⊢ (N \in ℕ \land x \in D) \to if (x \in \{0_{G}\}, ϕ (N), 0) = if (x = 0_{G}, ϕ (N), 0)$
27	23 26	eqtr4d	$⊢ (N \in ℕ \land x \in D) \to \sum_{a \in {Base}_{ℤ / N ℤ}} x (a) = if (x \in \{0_{G}\}, ϕ (N), 0)$
28	27	sumeq2dv	$⊢ N \in ℕ \to \sum_{x \in D} \sum_{a \in {Base}_{ℤ / N ℤ}} x (a) = \sum_{x \in D} if (x \in \{0_{G}\}, ϕ (N), 0)$
29	11 20 28	3eqtr3d	$⊢ N \in ℕ \to \sum_{a \in {Base}_{ℤ / N ℤ}} if (a \in \{1_{ℤ / N ℤ}\}, \|D\|, 0) = \sum_{x \in D} if (x \in \{0_{G}\}, ϕ (N), 0)$
30		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
31	3	zncrng	$⊢ N \in ℕ_{0} \to ℤ / N ℤ \in CRing$
32		crngring	$⊢ ℤ / N ℤ \in CRing \to ℤ / N ℤ \in Ring$
33	4 12	ringidcl	$⊢ ℤ / N ℤ \in Ring \to 1_{ℤ / N ℤ} \in {Base}_{ℤ / N ℤ}$
34	30 31 32 33	4syl	$⊢ N \in ℕ \to 1_{ℤ / N ℤ} \in {Base}_{ℤ / N ℤ}$
35	34	snssd	$⊢ N \in ℕ \to \{1_{ℤ / N ℤ}\} \subseteq {Base}_{ℤ / N ℤ}$
36		hashcl	$⊢ D \in Fin \to \|D\| \in ℕ_{0}$
37		nn0cn	$⊢ \|D\| \in ℕ_{0} \to \|D\| \in ℂ$
38	6 36 37	3syl	$⊢ N \in ℕ \to \|D\| \in ℂ$
39	38	ralrimivw	$⊢ N \in ℕ \to \forall a \in \{1_{ℤ / N ℤ}\} \|D\| \in ℂ$
40	5	olcd	$⊢ N \in ℕ \to ({Base}_{ℤ / N ℤ} \subseteq ℤ_{\geq 0} \lor {Base}_{ℤ / N ℤ} \in Fin)$
41		sumss2	$⊢ ((\{1_{ℤ / N ℤ}\} \subseteq {Base}_{ℤ / N ℤ} \land \forall a \in \{1_{ℤ / N ℤ}\} \|D\| \in ℂ) \land ({Base}_{ℤ / N ℤ} \subseteq ℤ_{\geq 0} \lor {Base}_{ℤ / N ℤ} \in Fin)) \to \sum_{a \in \{1_{ℤ / N ℤ}\}} \|D\| = \sum_{a \in {Base}_{ℤ / N ℤ}} if (a \in \{1_{ℤ / N ℤ}\}, \|D\|, 0)$
42	35 39 40 41	syl21anc	$⊢ N \in ℕ \to \sum_{a \in \{1_{ℤ / N ℤ}\}} \|D\| = \sum_{a \in {Base}_{ℤ / N ℤ}} if (a \in \{1_{ℤ / N ℤ}\}, \|D\|, 0)$
43	1	dchrabl	$⊢ N \in ℕ \to G \in Abel$
44		ablgrp	$⊢ G \in Abel \to G \in Grp$
45	2 21	grpidcl	$⊢ G \in Grp \to 0_{G} \in D$
46	43 44 45	3syl	$⊢ N \in ℕ \to 0_{G} \in D$
47	46	snssd	$⊢ N \in ℕ \to \{0_{G}\} \subseteq D$
48		phicl	$⊢ N \in ℕ \to ϕ (N) \in ℕ$
49	48	nncnd	$⊢ N \in ℕ \to ϕ (N) \in ℂ$
50	49	ralrimivw	$⊢ N \in ℕ \to \forall x \in \{0_{G}\} ϕ (N) \in ℂ$
51	6	olcd	$⊢ N \in ℕ \to (D \subseteq ℤ_{\geq 0} \lor D \in Fin)$
52		sumss2	$⊢ ((\{0_{G}\} \subseteq D \land \forall x \in \{0_{G}\} ϕ (N) \in ℂ) \land (D \subseteq ℤ_{\geq 0} \lor D \in Fin)) \to \sum_{x \in \{0_{G}\}} ϕ (N) = \sum_{x \in D} if (x \in \{0_{G}\}, ϕ (N), 0)$
53	47 50 51 52	syl21anc	$⊢ N \in ℕ \to \sum_{x \in \{0_{G}\}} ϕ (N) = \sum_{x \in D} if (x \in \{0_{G}\}, ϕ (N), 0)$
54	29 42 53	3eqtr4d	$⊢ N \in ℕ \to \sum_{a \in \{1_{ℤ / N ℤ}\}} \|D\| = \sum_{x \in \{0_{G}\}} ϕ (N)$
55		eqidd	$⊢ a = 1_{ℤ / N ℤ} \to \|D\| = \|D\|$
56	55	sumsn	$⊢ (1_{ℤ / N ℤ} \in {Base}_{ℤ / N ℤ} \land \|D\| \in ℂ) \to \sum_{a \in \{1_{ℤ / N ℤ}\}} \|D\| = \|D\|$
57	34 38 56	syl2anc	$⊢ N \in ℕ \to \sum_{a \in \{1_{ℤ / N ℤ}\}} \|D\| = \|D\|$
58		eqidd	$⊢ x = 0_{G} \to ϕ (N) = ϕ (N)$
59	58	sumsn	$⊢ (0_{G} \in D \land ϕ (N) \in ℂ) \to \sum_{x \in \{0_{G}\}} ϕ (N) = ϕ (N)$
60	46 49 59	syl2anc	$⊢ N \in ℕ \to \sum_{x \in \{0_{G}\}} ϕ (N) = ϕ (N)$
61	54 57 60	3eqtr3d	$⊢ N \in ℕ \to \|D\| = ϕ (N)$

Metamath Proof Explorer

Theorem dchrhash

Proof