Metamath Proof Explorer

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 = ( DChr ` N )
dchrabs.d 
|- D = ( Base ` G )
dchrabs.x 
|- ( ph -> X e. D )
dchrabs.z 
|- Z = ( Z/nZ ` N )
dchrabs.u 
|- U = ( Unit ` Z )
dchrabs.a 
|- ( ph -> A e. U )
Assertion dchrabs 
|- ( ph -> ( abs ` ( X ` A ) ) = 1 )

Proof

Step Hyp Ref Expression
1 dchrabs.g 
 |-  G = ( DChr ` N )
2 dchrabs.d 
 |-  D = ( Base ` G )
3 dchrabs.x 
 |-  ( ph -> X e. D )
4 dchrabs.z 
 |-  Z = ( Z/nZ ` N )
5 dchrabs.u 
 |-  U = ( Unit ` Z )
6 dchrabs.a 
 |-  ( ph -> A e. U )
7 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
8 1 4 2 7 3 dchrf 
 |-  ( ph -> X : ( Base ` Z ) --> CC )
9 7 5 unitss 
 |-  U C_ ( Base ` Z )
10 9 6 sselid 
 |-  ( ph -> A e. ( Base ` Z ) )
11 8 10 ffvelcdmd 
 |-  ( ph -> ( X ` A ) e. CC )
12 1 4 2 7 5 3 10 dchrn0 
 |-  ( ph -> ( ( X ` A ) =/= 0 <-> A e. U ) )
13 6 12 mpbird 
 |-  ( ph -> ( X ` A ) =/= 0 )
14 11 13 absrpcld 
 |-  ( ph -> ( abs ` ( X ` A ) ) e. RR+ )
15 1 2 dchrrcl 
 |-  ( X e. D -> N e. NN )
16 4 7 znfi 
 |-  ( N e. NN -> ( Base ` Z ) e. Fin )
17 3 15 16 3syl 
 |-  ( ph -> ( Base ` Z ) e. Fin )
18 ssfi 
 |-  ( ( ( Base ` Z ) e. Fin /\ U C_ ( Base ` Z ) ) -> U e. Fin )
19 17 9 18 sylancl 
 |-  ( ph -> U e. Fin )
20 hashcl 
 |-  ( U e. Fin -> ( # ` U ) e. NN0 )
21 19 20 syl 
 |-  ( ph -> ( # ` U ) e. NN0 )
22 21 nn0red 
 |-  ( ph -> ( # ` U ) e. RR )
23 22 recnd 
 |-  ( ph -> ( # ` U ) e. CC )
24 6 ne0d 
 |-  ( ph -> U =/= (/) )
25 hashnncl 
 |-  ( U e. Fin -> ( ( # ` U ) e. NN <-> U =/= (/) ) )
26 19 25 syl 
 |-  ( ph -> ( ( # ` U ) e. NN <-> U =/= (/) ) )
27 24 26 mpbird 
 |-  ( ph -> ( # ` U ) e. NN )
28 27 nnne0d 
 |-  ( ph -> ( # ` U ) =/= 0 )
29 23 28 reccld 
 |-  ( ph -> ( 1 / ( # ` U ) ) e. CC )
30 14 22 29 cxpmuld 
 |-  ( ph -> ( ( abs ` ( X ` A ) ) ^c ( ( # ` U ) x. ( 1 / ( # ` U ) ) ) ) = ( ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) ^c ( 1 / ( # ` U ) ) ) )
31 23 28 recidd 
 |-  ( ph -> ( ( # ` U ) x. ( 1 / ( # ` U ) ) ) = 1 )
32 31 oveq2d 
 |-  ( ph -> ( ( abs ` ( X ` A ) ) ^c ( ( # ` U ) x. ( 1 / ( # ` U ) ) ) ) = ( ( abs ` ( X ` A ) ) ^c 1 ) )
33 11 abscld 
 |-  ( ph -> ( abs ` ( X ` A ) ) e. RR )
34 33 recnd 
 |-  ( ph -> ( abs ` ( X ` A ) ) e. CC )
35 cxpexp 
 |-  ( ( ( abs ` ( X ` A ) ) e. CC /\ ( # ` U ) e. NN0 ) -> ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) = ( ( abs ` ( X ` A ) ) ^ ( # ` U ) ) )
36 34 21 35 syl2anc 
 |-  ( ph -> ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) = ( ( abs ` ( X ` A ) ) ^ ( # ` U ) ) )
37 11 21 absexpd 
 |-  ( ph -> ( abs ` ( ( X ` A ) ^ ( # ` U ) ) ) = ( ( abs ` ( X ` A ) ) ^ ( # ` U ) ) )
38 cnring 
 |-  CCfld e. Ring
39 cnfldbas 
 |-  CC = ( Base ` CCfld )
40 cnfld0 
 |-  0 = ( 0g ` CCfld )
41 cndrng 
 |-  CCfld e. DivRing
42 39 40 41 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
43 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
44 42 43 unitsubm 
 |-  ( CCfld e. Ring -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
45 38 44 mp1i 
 |-  ( ph -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) )
46 eldifsn 
 |-  ( ( X ` A ) e. ( CC \ { 0 } ) <-> ( ( X ` A ) e. CC /\ ( X ` A ) =/= 0 ) )
47 11 13 46 sylanbrc 
 |-  ( ph -> ( X ` A ) e. ( CC \ { 0 } ) )
48 eqid 
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
49 eqid 
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
50 eqid 
 |-  ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) = ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
51 48 49 50 submmulg 
 |-  ( ( ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ( # ` U ) e. NN0 /\ ( X ` A ) e. ( CC \ { 0 } ) ) -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) )
52 45 21 47 51 syl3anc 
 |-  ( ph -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) )
53 eqid 
 |-  ( ( mulGrp ` Z ) |`s U ) = ( ( mulGrp ` Z ) |`s U )
54 1 4 2 5 53 49 3 dchrghm 
 |-  ( ph -> ( X |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) )
55 21 nn0zd 
 |-  ( ph -> ( # ` U ) e. ZZ )
56 5 53 unitgrpbas 
 |-  U = ( Base ` ( ( mulGrp ` Z ) |`s U ) )
57 eqid 
 |-  ( .g ` ( ( mulGrp ` Z ) |`s U ) ) = ( .g ` ( ( mulGrp ` Z ) |`s U ) )
58 56 57 50 ghmmulg 
 |-  ( ( ( X |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ ( # ` U ) e. ZZ /\ A e. U ) -> ( ( X |` U ) ` ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( ( X |` U ) ` A ) ) )
59 54 55 6 58 syl3anc 
 |-  ( ph -> ( ( X |` U ) ` ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( ( X |` U ) ` A ) ) )
60 3 15 syl 
 |-  ( ph -> N e. NN )
61 60 nnnn0d 
 |-  ( ph -> N e. NN0 )
62 4 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
63 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
64 61 62 63 3syl 
 |-  ( ph -> Z e. Ring )
65 5 53 unitgrp 
 |-  ( Z e. Ring -> ( ( mulGrp ` Z ) |`s U ) e. Grp )
66 64 65 syl 
 |-  ( ph -> ( ( mulGrp ` Z ) |`s U ) e. Grp )
67 eqid 
 |-  ( od ` ( ( mulGrp ` Z ) |`s U ) ) = ( od ` ( ( mulGrp ` Z ) |`s U ) )
68 56 67 oddvds2 
 |-  ( ( ( ( mulGrp ` Z ) |`s U ) e. Grp /\ U e. Fin /\ A e. U ) -> ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) )
69 66 19 6 68 syl3anc 
 |-  ( ph -> ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) )
70 eqid 
 |-  ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) )
71 56 67 57 70 oddvds 
 |-  ( ( ( ( mulGrp ` Z ) |`s U ) e. Grp /\ A e. U /\ ( # ` U ) e. ZZ ) -> ( ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) <-> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) ) )
72 66 6 55 71 syl3anc 
 |-  ( ph -> ( ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) <-> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) ) )
73 69 72 mpbid 
 |-  ( ph -> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) )
74 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
75 5 53 74 unitgrpid 
 |-  ( Z e. Ring -> ( 1r ` Z ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) )
76 64 75 syl 
 |-  ( ph -> ( 1r ` Z ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) )
77 73 76 eqtr4d 
 |-  ( ph -> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 1r ` Z ) )
78 77 fveq2d 
 |-  ( ph -> ( ( X |` U ) ` ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) ) = ( ( X |` U ) ` ( 1r ` Z ) ) )
79 6 fvresd 
 |-  ( ph -> ( ( X |` U ) ` A ) = ( X ` A ) )
80 79 oveq2d 
 |-  ( ph -> ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( ( X |` U ) ` A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) )
81 59 78 80 3eqtr3d 
 |-  ( ph -> ( ( X |` U ) ` ( 1r ` Z ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) )
82 5 74 1unit 
 |-  ( Z e. Ring -> ( 1r ` Z ) e. U )
83 fvres 
 |-  ( ( 1r ` Z ) e. U -> ( ( X |` U ) ` ( 1r ` Z ) ) = ( X ` ( 1r ` Z ) ) )
84 64 82 83 3syl 
 |-  ( ph -> ( ( X |` U ) ` ( 1r ` Z ) ) = ( X ` ( 1r ` Z ) ) )
85 52 81 84 3eqtr2d 
 |-  ( ph -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( X ` ( 1r ` Z ) ) )
86 cnfldexp 
 |-  ( ( ( X ` A ) e. CC /\ ( # ` U ) e. NN0 ) -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( X ` A ) ^ ( # ` U ) ) )
87 11 21 86 syl2anc 
 |-  ( ph -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( X ` A ) ^ ( # ` U ) ) )
88 1 4 2 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
89 88 3 sselid 
 |-  ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
90 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
91 90 74 ringidval 
 |-  ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) )
92 cnfld1 
 |-  1 = ( 1r ` CCfld )
93 43 92 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
94 91 93 mhm0 
 |-  ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( X ` ( 1r ` Z ) ) = 1 )
95 89 94 syl 
 |-  ( ph -> ( X ` ( 1r ` Z ) ) = 1 )
96 85 87 95 3eqtr3d 
 |-  ( ph -> ( ( X ` A ) ^ ( # ` U ) ) = 1 )
97 96 fveq2d 
 |-  ( ph -> ( abs ` ( ( X ` A ) ^ ( # ` U ) ) ) = ( abs ` 1 ) )
98 abs1 
 |-  ( abs ` 1 ) = 1
99 97 98 eqtrdi 
 |-  ( ph -> ( abs ` ( ( X ` A ) ^ ( # ` U ) ) ) = 1 )
100 36 37 99 3eqtr2d 
 |-  ( ph -> ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) = 1 )
101 100 oveq1d 
 |-  ( ph -> ( ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) ^c ( 1 / ( # ` U ) ) ) = ( 1 ^c ( 1 / ( # ` U ) ) ) )
102 30 32 101 3eqtr3d 
 |-  ( ph -> ( ( abs ` ( X ` A ) ) ^c 1 ) = ( 1 ^c ( 1 / ( # ` U ) ) ) )
103 34 cxp1d 
 |-  ( ph -> ( ( abs ` ( X ` A ) ) ^c 1 ) = ( abs ` ( X ` A ) ) )
104 29 1cxpd 
 |-  ( ph -> ( 1 ^c ( 1 / ( # ` U ) ) ) = 1 )
105 102 103 104 3eqtr3d 
 |-  ( ph -> ( abs ` ( X ` A ) ) = 1 )