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 |
|
dchrisum0f.x |
|- ( ph -> X e. D ) |
9 |
|
dchrisum0flb.r |
|- ( ph -> X : ( Base ` Z ) --> RR ) |
10 |
|
fzfid |
|- ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. Fin ) |
11 |
|
dvdsssfz1 |
|- ( n e. NN -> { q e. NN | q || n } C_ ( 1 ... n ) ) |
12 |
11
|
adantl |
|- ( ( ph /\ n e. NN ) -> { q e. NN | q || n } C_ ( 1 ... n ) ) |
13 |
10 12
|
ssfid |
|- ( ( ph /\ n e. NN ) -> { q e. NN | q || n } e. Fin ) |
14 |
9
|
ad2antrr |
|- ( ( ( ph /\ n e. NN ) /\ m e. { q e. NN | q || n } ) -> X : ( Base ` Z ) --> RR ) |
15 |
3
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
16 |
|
eqid |
|- ( Base ` Z ) = ( Base ` Z ) |
17 |
1 16 2
|
znzrhfo |
|- ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) ) |
18 |
|
fof |
|- ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) ) |
19 |
15 17 18
|
3syl |
|- ( ph -> L : ZZ --> ( Base ` Z ) ) |
20 |
19
|
adantr |
|- ( ( ph /\ n e. NN ) -> L : ZZ --> ( Base ` Z ) ) |
21 |
|
elrabi |
|- ( m e. { q e. NN | q || n } -> m e. NN ) |
22 |
21
|
nnzd |
|- ( m e. { q e. NN | q || n } -> m e. ZZ ) |
23 |
|
ffvelrn |
|- ( ( L : ZZ --> ( Base ` Z ) /\ m e. ZZ ) -> ( L ` m ) e. ( Base ` Z ) ) |
24 |
20 22 23
|
syl2an |
|- ( ( ( ph /\ n e. NN ) /\ m e. { q e. NN | q || n } ) -> ( L ` m ) e. ( Base ` Z ) ) |
25 |
14 24
|
ffvelrnd |
|- ( ( ( ph /\ n e. NN ) /\ m e. { q e. NN | q || n } ) -> ( X ` ( L ` m ) ) e. RR ) |
26 |
13 25
|
fsumrecl |
|- ( ( ph /\ n e. NN ) -> sum_ m e. { q e. NN | q || n } ( X ` ( L ` m ) ) e. RR ) |
27 |
|
breq2 |
|- ( b = n -> ( q || b <-> q || n ) ) |
28 |
27
|
rabbidv |
|- ( b = n -> { q e. NN | q || b } = { q e. NN | q || n } ) |
29 |
28
|
sumeq1d |
|- ( b = n -> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) = sum_ v e. { q e. NN | q || n } ( X ` ( L ` v ) ) ) |
30 |
|
2fveq3 |
|- ( v = m -> ( X ` ( L ` v ) ) = ( X ` ( L ` m ) ) ) |
31 |
30
|
cbvsumv |
|- sum_ v e. { q e. NN | q || n } ( X ` ( L ` v ) ) = sum_ m e. { q e. NN | q || n } ( X ` ( L ` m ) ) |
32 |
29 31
|
eqtrdi |
|- ( b = n -> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) = sum_ m e. { q e. NN | q || n } ( X ` ( L ` m ) ) ) |
33 |
32
|
cbvmptv |
|- ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) ) = ( n e. NN |-> sum_ m e. { q e. NN | q || n } ( X ` ( L ` m ) ) ) |
34 |
7 33
|
eqtri |
|- F = ( n e. NN |-> sum_ m e. { q e. NN | q || n } ( X ` ( L ` m ) ) ) |
35 |
26 34
|
fmptd |
|- ( ph -> F : NN --> RR ) |