Theorem dchrabs

Description: A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrabs.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrabs.d	$$⊢D={\mathrm{Base}}_G$$
	dchrabs.x	$$⊢\phi \to X\in D$$
	dchrabs.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrabs.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	dchrabs.a	$$⊢\phi \to A\in U$$
Assertion	dchrabs	$$⊢\phi \to \left|X\left(A\right)\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		dchrabs.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrabs.d	$$⊢D={\mathrm{Base}}_G$$
3		dchrabs.x	$$⊢\phi \to X\in D$$
4		dchrabs.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
5		dchrabs.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
6		dchrabs.a	$$⊢\phi \to A\in U$$
7		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
8	1 4 2 7 3	dchrf	$$⊢\phi \to X:{\mathrm{Base}}_Z⟶ℂ$$
9	7 5	unitss	$$⊢U\subseteq {\mathrm{Base}}_Z$$
10	9 6	sseldi	$$⊢\phi \to A\in {\mathrm{Base}}_Z$$
11	8 10	ffvelrnd	$$⊢\phi \to X\left(A\right)\in ℂ$$
12	1 4 2 7 5 3 10	dchrn0	$$⊢\phi \to \left(X\left(A\right)\ne 0\leftrightarrow A\in U\right)$$
13	6 12	mpbird	$$⊢\phi \to X\left(A\right)\ne 0$$
14	11 13	absrpcld	$$⊢\phi \to \left|X\left(A\right)\right|\in {ℝ}^{+}$$
15	1 2	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
16	4 7	znfi	$$⊢N\in \mathbb{N}\to {\mathrm{Base}}_Z\in \mathrm{Fin}$$
17	3 15 16	3syl	$$⊢\phi \to {\mathrm{Base}}_Z\in \mathrm{Fin}$$
18		ssfi	$$⊢\left({\mathrm{Base}}_Z\in \mathrm{Fin}\wedge U\subseteq {\mathrm{Base}}_Z\right)\to U\in \mathrm{Fin}$$
19	17 9 18	sylancl	$$⊢\phi \to U\in \mathrm{Fin}$$
20		hashcl	$$⊢U\in \mathrm{Fin}\to \left|U\right|\in {\mathbb{N}}_0$$
21	19 20	syl	$$⊢\phi \to \left|U\right|\in {\mathbb{N}}_0$$
22	21	nn0red	$$⊢\phi \to \left|U\right|\in ℝ$$
23	22	recnd	$$⊢\phi \to \left|U\right|\in ℂ$$
24	6	ne0d	$$⊢\phi \to U\ne \varnothing$$
25		hashnncl	$$⊢U\in \mathrm{Fin}\to \left(\left|U\right|\in \mathbb{N}\leftrightarrow U\ne \varnothing \right)$$
26	19 25	syl	$$⊢\phi \to \left(\left|U\right|\in \mathbb{N}\leftrightarrow U\ne \varnothing \right)$$
27	24 26	mpbird	$$⊢\phi \to \left|U\right|\in \mathbb{N}$$
28	27	nnne0d	$$⊢\phi \to \left|U\right|\ne 0$$
29	23 28	reccld	$$⊢\phi \to \frac{1}{\left|U\right|}\in ℂ$$
30	14 22 29	cxpmuld	$$⊢\phi \to {\left|X\left(A\right)\right|}^{\left|U\right|\left(\frac{1}{\left|U\right|}\right)}={\left({\left|X\left(A\right)\right|}^{\left|U\right|}\right)}^{\frac{1}{\left|U\right|}}$$
31	23 28	recidd	$$⊢\phi \to \left|U\right|\left(\frac{1}{\left|U\right|}\right)=1$$
32	31	oveq2d	$$⊢\phi \to {\left|X\left(A\right)\right|}^{\left|U\right|\left(\frac{1}{\left|U\right|}\right)}={\left|X\left(A\right)\right|}^1$$
33	11	abscld	$$⊢\phi \to \left|X\left(A\right)\right|\in ℝ$$
34	33	recnd	$$⊢\phi \to \left|X\left(A\right)\right|\in ℂ$$
35		cxpexp	$$⊢\left(\left|X\left(A\right)\right|\in ℂ\wedge \left|U\right|\in {\mathbb{N}}_0\right)\to {\left|X\left(A\right)\right|}^{\left|U\right|}={\left|X\left(A\right)\right|}^{\left|U\right|}$$
36	34 21 35	syl2anc	$$⊢\phi \to {\left|X\left(A\right)\right|}^{\left|U\right|}={\left|X\left(A\right)\right|}^{\left|U\right|}$$
37	11 21	absexpd	$$⊢\phi \to \left|{X\left(A\right)}^{\left|U\right|}\right|={\left|X\left(A\right)\right|}^{\left|U\right|}$$
38		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
39		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
40		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
41		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
42	39 40 41	drngui	$$⊢ℂ\setminus \left\{0\right\}=\mathrm{Unit}\left({ℂ}_{\mathrm{fld}}\right)$$
43		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
44	42 43	unitsubm	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to ℂ\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
45	38 44	mp1i	$$⊢\phi \to ℂ\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
46		eldifsn	$$⊢X\left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(X\left(A\right)\in ℂ\wedge X\left(A\right)\ne 0\right)$$
47	11 13 46	sylanbrc	$$⊢\phi \to X\left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)$$
48		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}={\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
49		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
50		eqid	$$⊢{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}={\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}$$
51	48 49 50	submmulg	$$⊢\left(ℂ\setminus \left\{0\right\}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \left|U\right|\in {\mathbb{N}}_0\wedge X\left(A\right)\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to \left|U\right|{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}X\left(A\right)=\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}X\left(A\right)$$
52	45 21 47 51	syl3anc	$$⊢\phi \to \left|U\right|{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}X\left(A\right)=\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}X\left(A\right)$$
53		eqid	$$⊢{\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U={\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U$$
54	1 4 2 5 53 49 3	dchrghm	$$⊢\phi \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)$$
55	21	nn0zd	$$⊢\phi \to \left|U\right|\in \mathbb{Z}$$
56	5 53	unitgrpbas	$$⊢U={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}$$
57		eqid	$$⊢{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}={\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}$$
58	56 57 50	ghmmulg	$$⊢\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 \left|U\right|\in \mathbb{Z}\wedge A\in U\right)\to \left({X\upharpoonright }_U\right)\left(\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}A\right)=\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}\left({X\upharpoonright }_U\right)\left(A\right)$$
59	54 55 6 58	syl3anc	$$⊢\phi \to \left({X\upharpoonright }_U\right)\left(\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}A\right)=\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}\left({X\upharpoonright }_U\right)\left(A\right)$$
60	3 15	syl	$$⊢\phi \to N\in \mathbb{N}$$
61	60	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
62	4	zncrng	$$⊢N\in {\mathbb{N}}_0\to Z\in \mathrm{CRing}$$
63		crngring	$$⊢Z\in \mathrm{CRing}\to Z\in \mathrm{Ring}$$
64	61 62 63	3syl	$$⊢\phi \to Z\in \mathrm{Ring}$$
65	5 53	unitgrp	$$⊢Z\in \mathrm{Ring}\to {\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
66	64 65	syl	$$⊢\phi \to {\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
67		eqid	$$⊢\mathrm{od}\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)=\mathrm{od}\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)$$
68	56 67	oddvds2	$$⊢\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge U\in \mathrm{Fin}\wedge A\in U\right)\to \mathrm{od}\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)\left(A\right)\parallel \left|U\right|$$
69	66 19 6 68	syl3anc	$$⊢\phi \to \mathrm{od}\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)\left(A\right)\parallel \left|U\right|$$
70		eqid	$$⊢0_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}=0_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}$$
71	56 67 57 70	oddvds	$$⊢\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge A\in U\wedge \left|U\right|\in \mathbb{Z}\right)\to \left(\mathrm{od}\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)\left(A\right)\parallel \left|U\right|\leftrightarrow \left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}A=0_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}\right)$$
72	66 6 55 71	syl3anc	$$⊢\phi \to \left(\mathrm{od}\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)\left(A\right)\parallel \left|U\right|\leftrightarrow \left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}A=0_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}\right)$$
73	69 72	mpbid	$$⊢\phi \to \left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}A=0_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}$$
74		eqid	$$⊢1_Z=1_Z$$
75	5 53 74	unitgrpid	$$⊢Z\in \mathrm{Ring}\to 1_Z=0_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}$$
76	64 75	syl	$$⊢\phi \to 1_Z=0_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}$$
77	73 76	eqtr4d	$$⊢\phi \to \left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}A=1_Z$$
78	77	fveq2d	$$⊢\phi \to \left({X\upharpoonright }_U\right)\left(\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_Z{\upharpoonright }_{𝑠}U\right)}A\right)=\left({X\upharpoonright }_U\right)\left(1_Z\right)$$
79	6	fvresd	$$⊢\phi \to \left({X\upharpoonright }_U\right)\left(A\right)=X\left(A\right)$$
80	79	oveq2d	$$⊢\phi \to \left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}\left({X\upharpoonright }_U\right)\left(A\right)=\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}X\left(A\right)$$
81	59 78 80	3eqtr3d	$$⊢\phi \to \left({X\upharpoonright }_U\right)\left(1_Z\right)=\left|U\right|{\cdot }_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)}X\left(A\right)$$
82	5 74	1unit	$$⊢Z\in \mathrm{Ring}\to 1_Z\in U$$
83		fvres	$$⊢1_Z\in U\to \left({X\upharpoonright }_U\right)\left(1_Z\right)=X\left(1_Z\right)$$
84	64 82 83	3syl	$$⊢\phi \to \left({X\upharpoonright }_U\right)\left(1_Z\right)=X\left(1_Z\right)$$
85	52 81 84	3eqtr2d	$$⊢\phi \to \left|U\right|{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}X\left(A\right)=X\left(1_Z\right)$$
86		cnfldexp	$$⊢\left(X\left(A\right)\in ℂ\wedge \left|U\right|\in {\mathbb{N}}_0\right)\to \left|U\right|{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}X\left(A\right)={X\left(A\right)}^{\left|U\right|}$$
87	11 21 86	syl2anc	$$⊢\phi \to \left|U\right|{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}X\left(A\right)={X\left(A\right)}^{\left|U\right|}$$
88	1 4 2	dchrmhm	$$⊢D\subseteq {\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
89	88 3	sseldi	$$⊢\phi \to X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$$
90		eqid	$$⊢{\mathrm{mulGrp}}_Z={\mathrm{mulGrp}}_Z$$
91	90 74	ringidval	$$⊢1_Z=0_{{\mathrm{mulGrp}}_Z}$$
92		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
93	43 92	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
94	91 93	mhm0	$$⊢X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\to X\left(1_Z\right)=1$$
95	89 94	syl	$$⊢\phi \to X\left(1_Z\right)=1$$
96	85 87 95	3eqtr3d	$$⊢\phi \to {X\left(A\right)}^{\left|U\right|}=1$$
97	96	fveq2d	$$⊢\phi \to \left|{X\left(A\right)}^{\left|U\right|}\right|=\left|1\right|$$
98		abs1	$$⊢\left|1\right|=1$$
99	97 98	syl6eq	$$⊢\phi \to \left|{X\left(A\right)}^{\left|U\right|}\right|=1$$
100	36 37 99	3eqtr2d	$$⊢\phi \to {\left|X\left(A\right)\right|}^{\left|U\right|}=1$$
101	100	oveq1d	$$⊢\phi \to {\left({\left|X\left(A\right)\right|}^{\left|U\right|}\right)}^{\frac{1}{\left|U\right|}}=1^{\frac{1}{\left|U\right|}}$$
102	30 32 101	3eqtr3d	$$⊢\phi \to {\left|X\left(A\right)\right|}^1=1^{\frac{1}{\left|U\right|}}$$
103	34	cxp1d	$$⊢\phi \to {\left|X\left(A\right)\right|}^1=\left|X\left(A\right)\right|$$
104	29	1cxpd	$$⊢\phi \to 1^{\frac{1}{\left|U\right|}}=1$$
105	102 103 104	3eqtr3d	$$⊢\phi \to \left|X\left(A\right)\right|=1$$