Theorem dchrisum0ff

Description: The function F is a real function. (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	rpvmasum.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
	rpvmasum.a	$$⊢\phi \to N\in \mathbb{N}$$
	rpvmasum2.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	rpvmasum2.d	$$⊢D={\mathrm{Base}}_G$$
	rpvmasum2.1	$$⊢\underset{\dot{}}{1}=0_G$$
	dchrisum0f.f	$$⊢F=\left(b\in \mathbb{N}⟼\sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)\right)$$
	dchrisum0f.x	$$⊢\phi \to X\in D$$
	dchrisum0flb.r	$$⊢\phi \to X:{\mathrm{Base}}_Z⟶ℝ$$
Assertion	dchrisum0ff	$$⊢\phi \to F:\mathbb{N}⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
2		rpvmasum.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(Z\right)$$
3		rpvmasum.a	$$⊢\phi \to N\in \mathbb{N}$$
4		rpvmasum2.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
5		rpvmasum2.d	$$⊢D={\mathrm{Base}}_G$$
6		rpvmasum2.1	$$⊢\underset{\dot{}}{1}=0_G$$
7		dchrisum0f.f	$$⊢F=\left(b\in \mathbb{N}⟼\sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)\right)$$
8		dchrisum0f.x	$$⊢\phi \to X\in D$$
9		dchrisum0flb.r	$$⊢\phi \to X:{\mathrm{Base}}_Z⟶ℝ$$
10		fzfid	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(1\dots n\right)\in \mathrm{Fin}$$
11		dvdsssfz1	$$⊢n\in \mathbb{N}\to \left\{q\in \mathbb{N}|q\parallel n\right\}\subseteq \left(1\dots n\right)$$
12	11	adantl	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left\{q\in \mathbb{N}|q\parallel n\right\}\subseteq \left(1\dots n\right)$$
13	10 12	ssfid	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left\{q\in \mathbb{N}|q\parallel n\right\}\in \mathrm{Fin}$$
14	9	ad2antrr	$$⊢\left(\left(\phi \wedge n\in \mathbb{N}\right)\wedge m\in \left\{q\in \mathbb{N}|q\parallel n\right\}\right)\to X:{\mathrm{Base}}_Z⟶ℝ$$
15	3	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
16		eqid	$$⊢{\mathrm{Base}}_Z={\mathrm{Base}}_Z$$
17	1 16 2	znzrhfo	$$⊢N\in {\mathbb{N}}_0\to L:\mathbb{Z}\underset{onto}{⟶}{\mathrm{Base}}_Z$$
18		fof	$$⊢L:\mathbb{Z}\underset{onto}{⟶}{\mathrm{Base}}_Z\to L:\mathbb{Z}⟶{\mathrm{Base}}_Z$$
19	15 17 18	3syl	$$⊢\phi \to L:\mathbb{Z}⟶{\mathrm{Base}}_Z$$
20	19	adantr	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to L:\mathbb{Z}⟶{\mathrm{Base}}_Z$$
21		elrabi	$$⊢m\in \left\{q\in \mathbb{N}|q\parallel n\right\}\to m\in \mathbb{N}$$
22	21	nnzd	$$⊢m\in \left\{q\in \mathbb{N}|q\parallel n\right\}\to m\in \mathbb{Z}$$
23		ffvelcdm	$$⊢\left(L:\mathbb{Z}⟶{\mathrm{Base}}_Z\wedge m\in \mathbb{Z}\right)\to L\left(m\right)\in {\mathrm{Base}}_Z$$
24	20 22 23	syl2an	$$⊢\left(\left(\phi \wedge n\in \mathbb{N}\right)\wedge m\in \left\{q\in \mathbb{N}|q\parallel n\right\}\right)\to L\left(m\right)\in {\mathrm{Base}}_Z$$
25	14 24	ffvelcdmd	$$⊢\left(\left(\phi \wedge n\in \mathbb{N}\right)\wedge m\in \left\{q\in \mathbb{N}|q\parallel n\right\}\right)\to X\left(L\left(m\right)\right)\in ℝ$$
26	13 25	fsumrecl	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \sum _{m\in \left\{q\in \mathbb{N}|q\parallel n\right\}}X\left(L\left(m\right)\right)\in ℝ$$
27		breq2	$$⊢b=n\to \left(q\parallel b\leftrightarrow q\parallel n\right)$$
28	27	rabbidv	$$⊢b=n\to \left\{q\in \mathbb{N}|q\parallel b\right\}=\left\{q\in \mathbb{N}|q\parallel n\right\}$$
29	28	sumeq1d	$$⊢b=n\to \sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)=\sum _{v\in \left\{q\in \mathbb{N}|q\parallel n\right\}}X\left(L\left(v\right)\right)$$
30		2fveq3	$$⊢v=m\to X\left(L\left(v\right)\right)=X\left(L\left(m\right)\right)$$
31	30	cbvsumv	$$⊢\sum _{v\in \left\{q\in \mathbb{N}|q\parallel n\right\}}X\left(L\left(v\right)\right)=\sum _{m\in \left\{q\in \mathbb{N}|q\parallel n\right\}}X\left(L\left(m\right)\right)$$
32	29 31	eqtrdi	$$⊢b=n\to \sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)=\sum _{m\in \left\{q\in \mathbb{N}|q\parallel n\right\}}X\left(L\left(m\right)\right)$$
33	32	cbvmptv	$$⊢\left(b\in \mathbb{N}⟼\sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)\right)=\left(n\in \mathbb{N}⟼\sum _{m\in \left\{q\in \mathbb{N}|q\parallel n\right\}}X\left(L\left(m\right)\right)\right)$$
34	7 33	eqtri	$$⊢F=\left(n\in \mathbb{N}⟼\sum _{m\in \left\{q\in \mathbb{N}|q\parallel n\right\}}X\left(L\left(m\right)\right)\right)$$
35	26 34	fmptd	$$⊢\phi \to F:\mathbb{N}⟶ℝ$$