Metamath Proof Explorer

Theorem dchrisum0ff

Description: The function F is a real function. (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 ) ) )
dchrisum0f.x 
|- ( ph -> X e. D )
dchrisum0flb.r 
|- ( ph -> X : ( Base ` Z ) --> RR )
Assertion dchrisum0ff 
|- ( ph -> F : NN --> RR )

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