This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrisum0fval

Description: Value of the function F , the divisor sum of a Dirichlet character. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum2.g 
|- G = ( DChr ` N )
rpvmasum2.d 
|- D = ( Base ` G )
rpvmasum2.1 
|- .1. = ( 0g ` G )
dchrisum0f.f 
|- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
Assertion dchrisum0fval 
|- ( A e. NN -> ( F ` A ) = sum_ t e. { q e. NN | q || A } ( X ` ( L ` t ) ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum2.g 
 |-  G = ( DChr ` N )
5 rpvmasum2.d 
 |-  D = ( Base ` G )
6 rpvmasum2.1 
 |-  .1. = ( 0g ` G )
7 dchrisum0f.f 
 |-  F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
8 breq2 
 |-  ( b = A -> ( q || b <-> q || A ) )
9 8 rabbidv 
 |-  ( b = A -> { q e. NN | q || b } = { q e. NN | q || A } )
10 9 sumeq1d 
 |-  ( b = A -> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) = sum_ v e. { q e. NN | q || A } ( X ` ( L ` v ) ) )
11 2fveq3 
 |-  ( v = t -> ( X ` ( L ` v ) ) = ( X ` ( L ` t ) ) )
12 11 cbvsumv 
 |-  sum_ v e. { q e. NN | q || A } ( X ` ( L ` v ) ) = sum_ t e. { q e. NN | q || A } ( X ` ( L ` t ) )
13 10 12 eqtrdi 
 |-  ( b = A -> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) = sum_ t e. { q e. NN | q || A } ( X ` ( L ` t ) ) )
14 sumex 
 |-  sum_ t e. { q e. NN | q || A } ( X ` ( L ` t ) ) e. _V
15 13 7 14 fvmpt 
 |-  ( A e. NN -> ( F ` A ) = sum_ t e. { q e. NN | q || A } ( X ` ( L ` t ) ) )