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