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