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 )