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 ffvelrnd
 |-  ( 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 )