Metamath Proof Explorer


Theorem sum2dchr

Description: An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Part of Theorem 6.5.2 of Shapiro p. 232. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sum2dchr.g
|- G = ( DChr ` N )
sum2dchr.d
|- D = ( Base ` G )
sum2dchr.z
|- Z = ( Z/nZ ` N )
sum2dchr.b
|- B = ( Base ` Z )
sum2dchr.u
|- U = ( Unit ` Z )
sum2dchr.n
|- ( ph -> N e. NN )
sum2dchr.a
|- ( ph -> A e. B )
sum2dchr.c
|- ( ph -> C e. U )
Assertion sum2dchr
|- ( ph -> sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) = if ( A = C , ( phi ` N ) , 0 ) )

Proof

Step Hyp Ref Expression
1 sum2dchr.g
 |-  G = ( DChr ` N )
2 sum2dchr.d
 |-  D = ( Base ` G )
3 sum2dchr.z
 |-  Z = ( Z/nZ ` N )
4 sum2dchr.b
 |-  B = ( Base ` Z )
5 sum2dchr.u
 |-  U = ( Unit ` Z )
6 sum2dchr.n
 |-  ( ph -> N e. NN )
7 sum2dchr.a
 |-  ( ph -> A e. B )
8 sum2dchr.c
 |-  ( ph -> C e. U )
9 eqid
 |-  ( 1r ` Z ) = ( 1r ` Z )
10 6 nnnn0d
 |-  ( ph -> N e. NN0 )
11 3 zncrng
 |-  ( N e. NN0 -> Z e. CRing )
12 crngring
 |-  ( Z e. CRing -> Z e. Ring )
13 10 11 12 3syl
 |-  ( ph -> Z e. Ring )
14 eqid
 |-  ( /r ` Z ) = ( /r ` Z )
15 4 5 14 dvrcl
 |-  ( ( Z e. Ring /\ A e. B /\ C e. U ) -> ( A ( /r ` Z ) C ) e. B )
16 13 7 8 15 syl3anc
 |-  ( ph -> ( A ( /r ` Z ) C ) e. B )
17 1 2 3 9 4 6 16 sumdchr
 |-  ( ph -> sum_ x e. D ( x ` ( A ( /r ` Z ) C ) ) = if ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) , ( phi ` N ) , 0 ) )
18 eqid
 |-  ( .r ` Z ) = ( .r ` Z )
19 eqid
 |-  ( invr ` Z ) = ( invr ` Z )
20 4 18 5 19 14 dvrval
 |-  ( ( A e. B /\ C e. U ) -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) )
21 7 8 20 syl2anc
 |-  ( ph -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) )
22 21 adantr
 |-  ( ( ph /\ x e. D ) -> ( A ( /r ` Z ) C ) = ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) )
23 22 fveq2d
 |-  ( ( ph /\ x e. D ) -> ( x ` ( A ( /r ` Z ) C ) ) = ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) )
24 1 3 2 dchrmhm
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
25 simpr
 |-  ( ( ph /\ x e. D ) -> x e. D )
26 24 25 sselid
 |-  ( ( ph /\ x e. D ) -> x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
27 7 adantr
 |-  ( ( ph /\ x e. D ) -> A e. B )
28 4 5 unitss
 |-  U C_ B
29 5 19 unitinvcl
 |-  ( ( Z e. Ring /\ C e. U ) -> ( ( invr ` Z ) ` C ) e. U )
30 13 8 29 syl2anc
 |-  ( ph -> ( ( invr ` Z ) ` C ) e. U )
31 30 adantr
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` Z ) ` C ) e. U )
32 28 31 sselid
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` Z ) ` C ) e. B )
33 eqid
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
34 33 4 mgpbas
 |-  B = ( Base ` ( mulGrp ` Z ) )
35 33 18 mgpplusg
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
36 eqid
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
37 cnfldmul
 |-  x. = ( .r ` CCfld )
38 36 37 mgpplusg
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
39 34 35 38 mhmlin
 |-  ( ( x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A e. B /\ ( ( invr ` Z ) ` C ) e. B ) -> ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) )
40 26 27 32 39 syl3anc
 |-  ( ( ph /\ x e. D ) -> ( x ` ( A ( .r ` Z ) ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) )
41 eqid
 |-  ( ( mulGrp ` Z ) |`s U ) = ( ( mulGrp ` Z ) |`s U )
42 eqid
 |-  ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
43 1 3 2 5 41 42 25 dchrghm
 |-  ( ( ph /\ x e. D ) -> ( x |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) )
44 8 adantr
 |-  ( ( ph /\ x e. D ) -> C e. U )
45 5 41 unitgrpbas
 |-  U = ( Base ` ( ( mulGrp ` Z ) |`s U ) )
46 5 41 19 invrfval
 |-  ( invr ` Z ) = ( invg ` ( ( mulGrp ` Z ) |`s U ) )
47 cnfldbas
 |-  CC = ( Base ` CCfld )
48 cnfld0
 |-  0 = ( 0g ` CCfld )
49 cndrng
 |-  CCfld e. DivRing
50 47 48 49 drngui
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
51 eqid
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
52 50 42 51 invrfval
 |-  ( invr ` CCfld ) = ( invg ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
53 45 46 52 ghminv
 |-  ( ( ( x |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ C e. U ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) )
54 43 44 53 syl2anc
 |-  ( ( ph /\ x e. D ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) )
55 31 fvresd
 |-  ( ( ph /\ x e. D ) -> ( ( x |` U ) ` ( ( invr ` Z ) ` C ) ) = ( x ` ( ( invr ` Z ) ` C ) ) )
56 44 fvresd
 |-  ( ( ph /\ x e. D ) -> ( ( x |` U ) ` C ) = ( x ` C ) )
57 56 fveq2d
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) = ( ( invr ` CCfld ) ` ( x ` C ) ) )
58 1 3 2 4 25 dchrf
 |-  ( ( ph /\ x e. D ) -> x : B --> CC )
59 28 44 sselid
 |-  ( ( ph /\ x e. D ) -> C e. B )
60 58 59 ffvelrnd
 |-  ( ( ph /\ x e. D ) -> ( x ` C ) e. CC )
61 1 3 2 4 5 25 59 dchrn0
 |-  ( ( ph /\ x e. D ) -> ( ( x ` C ) =/= 0 <-> C e. U ) )
62 44 61 mpbird
 |-  ( ( ph /\ x e. D ) -> ( x ` C ) =/= 0 )
63 cnfldinv
 |-  ( ( ( x ` C ) e. CC /\ ( x ` C ) =/= 0 ) -> ( ( invr ` CCfld ) ` ( x ` C ) ) = ( 1 / ( x ` C ) ) )
64 60 62 63 syl2anc
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( x ` C ) ) = ( 1 / ( x ` C ) ) )
65 recval
 |-  ( ( ( x ` C ) e. CC /\ ( x ` C ) =/= 0 ) -> ( 1 / ( x ` C ) ) = ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) )
66 60 62 65 syl2anc
 |-  ( ( ph /\ x e. D ) -> ( 1 / ( x ` C ) ) = ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) )
67 1 2 25 3 5 44 dchrabs
 |-  ( ( ph /\ x e. D ) -> ( abs ` ( x ` C ) ) = 1 )
68 67 oveq1d
 |-  ( ( ph /\ x e. D ) -> ( ( abs ` ( x ` C ) ) ^ 2 ) = ( 1 ^ 2 ) )
69 sq1
 |-  ( 1 ^ 2 ) = 1
70 68 69 eqtrdi
 |-  ( ( ph /\ x e. D ) -> ( ( abs ` ( x ` C ) ) ^ 2 ) = 1 )
71 70 oveq2d
 |-  ( ( ph /\ x e. D ) -> ( ( * ` ( x ` C ) ) / ( ( abs ` ( x ` C ) ) ^ 2 ) ) = ( ( * ` ( x ` C ) ) / 1 ) )
72 60 cjcld
 |-  ( ( ph /\ x e. D ) -> ( * ` ( x ` C ) ) e. CC )
73 72 div1d
 |-  ( ( ph /\ x e. D ) -> ( ( * ` ( x ` C ) ) / 1 ) = ( * ` ( x ` C ) ) )
74 66 71 73 3eqtrd
 |-  ( ( ph /\ x e. D ) -> ( 1 / ( x ` C ) ) = ( * ` ( x ` C ) ) )
75 57 64 74 3eqtrd
 |-  ( ( ph /\ x e. D ) -> ( ( invr ` CCfld ) ` ( ( x |` U ) ` C ) ) = ( * ` ( x ` C ) ) )
76 54 55 75 3eqtr3d
 |-  ( ( ph /\ x e. D ) -> ( x ` ( ( invr ` Z ) ` C ) ) = ( * ` ( x ` C ) ) )
77 76 oveq2d
 |-  ( ( ph /\ x e. D ) -> ( ( x ` A ) x. ( x ` ( ( invr ` Z ) ` C ) ) ) = ( ( x ` A ) x. ( * ` ( x ` C ) ) ) )
78 23 40 77 3eqtrd
 |-  ( ( ph /\ x e. D ) -> ( x ` ( A ( /r ` Z ) C ) ) = ( ( x ` A ) x. ( * ` ( x ` C ) ) ) )
79 78 sumeq2dv
 |-  ( ph -> sum_ x e. D ( x ` ( A ( /r ` Z ) C ) ) = sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) )
80 4 5 14 9 dvreq1
 |-  ( ( Z e. Ring /\ A e. B /\ C e. U ) -> ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) <-> A = C ) )
81 13 7 8 80 syl3anc
 |-  ( ph -> ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) <-> A = C ) )
82 81 ifbid
 |-  ( ph -> if ( ( A ( /r ` Z ) C ) = ( 1r ` Z ) , ( phi ` N ) , 0 ) = if ( A = C , ( phi ` N ) , 0 ) )
83 17 79 82 3eqtr3d
 |-  ( ph -> sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) = if ( A = C , ( phi ` N ) , 0 ) )