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 = /N
rpvmasum.l L = ℤRHom Z
rpvmasum.a φ N
rpvmasum2.g G = DChr N
rpvmasum2.d D = Base G
rpvmasum2.1 1 ˙ = 0 G
dchrisum0f.f F = b v q | q b X L v
dchrisum0f.x φ X D
dchrisum0flb.r φ X : Base Z
Assertion dchrisum0ff φ F :

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z = /N
2 rpvmasum.l L = ℤRHom Z
3 rpvmasum.a φ N
4 rpvmasum2.g G = DChr N
5 rpvmasum2.d D = Base G
6 rpvmasum2.1 1 ˙ = 0 G
7 dchrisum0f.f F = b v q | q b X L v
8 dchrisum0f.x φ X D
9 dchrisum0flb.r φ X : Base Z
10 fzfid φ n 1 n Fin
11 dvdsssfz1 n q | q n 1 n
12 11 adantl φ n q | q n 1 n
13 10 12 ssfid φ n q | q n Fin
14 9 ad2antrr φ n m q | q n X : Base Z
15 3 nnnn0d φ N 0
16 eqid Base Z = Base Z
17 1 16 2 znzrhfo N 0 L : onto Base Z
18 fof L : onto Base Z L : Base Z
19 15 17 18 3syl φ L : Base Z
20 19 adantr φ n L : Base Z
21 elrabi m q | q n m
22 21 nnzd m q | q n m
23 ffvelrn L : Base Z m L m Base Z
24 20 22 23 syl2an φ n m q | q n L m Base Z
25 14 24 ffvelrnd φ n m q | q n X L m
26 13 25 fsumrecl φ n m q | q n X L m
27 breq2 b = n q b q n
28 27 rabbidv b = n q | q b = q | q n
29 28 sumeq1d b = n v q | q b X L v = v q | q n X L v
30 2fveq3 v = m X L v = X L m
31 30 cbvsumv v q | q n X L v = m q | q n X L m
32 29 31 eqtrdi b = n v q | q b X L v = m q | q n X L m
33 32 cbvmptv b v q | q b X L v = n m q | q n X L m
34 7 33 eqtri F = n m q | q n X L m
35 26 34 fmptd φ F :