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 = /N
rpvmasum.l L = ℤRHom Z
rpvmasum.a φ N
rpvmasum2.g G = DChr N
rpvmasum2.d D = Base G
rpvmasum2.1 1 ˙ = 0 G
dchrisum0f.f F = b v q | q b X L v
Assertion dchrisum0fval A F A = t q | q A X L t

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z = /N
2 rpvmasum.l L = ℤRHom Z
3 rpvmasum.a φ N
4 rpvmasum2.g G = DChr N
5 rpvmasum2.d D = Base G
6 rpvmasum2.1 1 ˙ = 0 G
7 dchrisum0f.f F = b v q | q b X L v
8 breq2 b = A q b q A
9 8 rabbidv b = A q | q b = q | q A
10 9 sumeq1d b = A v q | q b X L v = v q | q A X L v
11 2fveq3 v = t X L v = X L t
12 11 cbvsumv v q | q A X L v = t q | q A X L t
13 10 12 eqtrdi b = A v q | q b X L v = t q | q A X L t
14 sumex t q | q A X L t V
15 13 7 14 fvmpt A F A = t q | q A X L t