Theorem dchrabs

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

	Ref	Expression
Hypotheses	dchrabs.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrabs.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrabs.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrabs.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrabs.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchrabs.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	dchrabs	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		dchrabs.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrabs.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
3		dchrabs.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
4		dchrabs.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
5		dchrabs.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
6		dchrabs.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
8	1 4 2 7 3	dchrf	⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
9	7 5	unitss	⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
10	9 6	sselid	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑍 ) )
11	8 10	ffvelcdmd	⊢ ( 𝜑 → ( 𝑋 ‘ 𝐴 ) ∈ ℂ )
12	1 4 2 7 5 3 10	dchrn0	⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ∈ 𝑈 ) )
13	6 12	mpbird	⊢ ( 𝜑 → ( 𝑋 ‘ 𝐴 ) ≠ 0 )
14	11 13	absrpcld	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℝ+ )
15	1 2	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
16	4 7	znfi	⊢ ( 𝑁 ∈ ℕ → ( Base ‘ 𝑍 ) ∈ Fin )
17	3 15 16	3syl	⊢ ( 𝜑 → ( Base ‘ 𝑍 ) ∈ Fin )
18		ssfi	⊢ ( ( ( Base ‘ 𝑍 ) ∈ Fin ∧ 𝑈 ⊆ ( Base ‘ 𝑍 ) ) → 𝑈 ∈ Fin )
19	17 9 18	sylancl	⊢ ( 𝜑 → 𝑈 ∈ Fin )
20		hashcl	⊢ ( 𝑈 ∈ Fin → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
21	19 20	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
22	21	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℝ )
23	22	recnd	⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℂ )
24	6	ne0d	⊢ ( 𝜑 → 𝑈 ≠ ∅ )
25		hashnncl	⊢ ( 𝑈 ∈ Fin → ( ( ♯ ‘ 𝑈 ) ∈ ℕ ↔ 𝑈 ≠ ∅ ) )
26	19 25	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ∈ ℕ ↔ 𝑈 ≠ ∅ ) )
27	24 26	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℕ )
28	27	nnne0d	⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ≠ 0 )
29	23 28	reccld	⊢ ( 𝜑 → ( 1 / ( ♯ ‘ 𝑈 ) ) ∈ ℂ )
30	14 22 29	cxpmuld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ( ♯ ‘ 𝑈 ) · ( 1 / ( ♯ ‘ 𝑈 ) ) ) ) = ( ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) )
31	23 28	recidd	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) · ( 1 / ( ♯ ‘ 𝑈 ) ) ) = 1 )
32	31	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ( ♯ ‘ 𝑈 ) · ( 1 / ( ♯ ‘ 𝑈 ) ) ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 1 ) )
33	11	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℝ )
34	33	recnd	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℂ )
35		cxpexp	⊢ ( ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑ ( ♯ ‘ 𝑈 ) ) )
36	34 21 35	syl2anc	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑ ( ♯ ‘ 𝑈 ) ) )
37	11 21	absexpd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑ ( ♯ ‘ 𝑈 ) ) )
38		cnring	⊢ ℂfld ∈ Ring
39		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
40		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
41		cndrng	⊢ ℂfld ∈ DivRing
42	39 40 41	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
43		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
44	42 43	unitsubm	⊢ ( ℂfld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
45	38 44	mp1i	⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
46		eldifsn	⊢ ( ( 𝑋 ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 ‘ 𝐴 ) ∈ ℂ ∧ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) )
47	11 13 46	sylanbrc	⊢ ( 𝜑 → ( 𝑋 ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) )
48		eqid	⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
49		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
50		eqid	⊢ ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) = ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) )
51	48 49 50	submmulg	⊢ ( ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ∧ ( 𝑋 ‘ 𝐴 ) ∈ ( ℂ ∖ { 0 } ) ) → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
52	45 21 47 51	syl3anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
53		eqid	⊢ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
54	1 4 2 5 53 49 3	dchrghm	⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) )
55	21	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℤ )
56	5 53	unitgrpbas	⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
57		eqid	⊢ ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) = ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
58	56 57 50	ghmmulg	⊢ ( ( ( 𝑋 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ∧ ( ♯ ‘ 𝑈 ) ∈ ℤ ∧ 𝐴 ∈ 𝑈 ) → ( ( 𝑋 ↾ 𝑈 ) ‘ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) ) )
59	54 55 6 58	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) ) )
60	3 15	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
61	60	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
62	4	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
63		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
64	61 62 63	3syl	⊢ ( 𝜑 → 𝑍 ∈ Ring )
65	5 53	unitgrp	⊢ ( 𝑍 ∈ Ring → ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp )
66	64 65	syl	⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp )
67		eqid	⊢ ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) = ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
68	56 67	oddvds2	⊢ ( ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑈 ∈ Fin ∧ 𝐴 ∈ 𝑈 ) → ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) )
69	66 19 6 68	syl3anc	⊢ ( 𝜑 → ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) )
70		eqid	⊢ ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
71	56 67 57 70	oddvds	⊢ ( ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp ∧ 𝐴 ∈ 𝑈 ∧ ( ♯ ‘ 𝑈 ) ∈ ℤ ) → ( ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) ↔ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ) )
72	66 6 55 71	syl3anc	⊢ ( 𝜑 → ( ( ( od ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑈 ) ↔ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) ) )
73	69 72	mpbid	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) )
74		eqid	⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
75	5 53 74	unitgrpid	⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) )
76	64 75	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑍 ) = ( 0g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) )
77	73 76	eqtr4d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) = ( 1r ‘ 𝑍 ) )
78	77	fveq2d	⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) 𝐴 ) ) = ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) )
79	6	fvresd	⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) = ( 𝑋 ‘ 𝐴 ) )
80	79	oveq2d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( ( 𝑋 ↾ 𝑈 ) ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
81	59 78 80	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) = ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ( 𝑋 ‘ 𝐴 ) ) )
82	5 74	1unit	⊢ ( 𝑍 ∈ Ring → ( 1r ‘ 𝑍 ) ∈ 𝑈 )
83		fvres	⊢ ( ( 1r ‘ 𝑍 ) ∈ 𝑈 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
84	64 82 83	3syl	⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ‘ ( 1r ‘ 𝑍 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
85	52 81 84	3eqtr2d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
86		cnfldexp	⊢ ( ( ( 𝑋 ‘ 𝐴 ) ∈ ℂ ∧ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) )
87	11 21 86	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑋 ‘ 𝐴 ) ) = ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) )
88	1 4 2	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
89	88 3	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
90		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
91	90 74	ringidval	⊢ ( 1r ‘ 𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
92		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
93	43 92	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
94	91 93	mhm0	⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
95	89 94	syl	⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
96	85 87 95	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) = 1 )
97	96	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) ) = ( abs ‘ 1 ) )
98		abs1	⊢ ( abs ‘ 1 ) = 1
99	97 98	eqtrdi	⊢ ( 𝜑 → ( abs ‘ ( ( 𝑋 ‘ 𝐴 ) ↑ ( ♯ ‘ 𝑈 ) ) ) = 1 )
100	36 37 99	3eqtr2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) = 1 )
101	100	oveq1d	⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 ( ♯ ‘ 𝑈 ) ) ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) = ( 1 ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) )
102	30 32 101	3eqtr3d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 1 ) = ( 1 ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) )
103	34	cxp1d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ↑𝑐 1 ) = ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) )
104	29	1cxpd	⊢ ( 𝜑 → ( 1 ↑𝑐 ( 1 / ( ♯ ‘ 𝑈 ) ) ) = 1 )
105	102 103 104	3eqtr3d	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) = 1 )