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