Theorem dchrisum0fval

Description: Value of the function F , the divisor sum of a Dirichlet character. (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)$$
Assertion	dchrisum0fval	$$⊢A\in \mathbb{N}\to F\left(A\right)=\sum _{t\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(t\right)\right)$$

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		breq2	$$⊢b=A\to \left(q\parallel b\leftrightarrow q\parallel A\right)$$
9	8	rabbidv	$$⊢b=A\to \left\{q\in \mathbb{N}|q\parallel b\right\}=\left\{q\in \mathbb{N}|q\parallel A\right\}$$
10	9	sumeq1d	$$⊢b=A\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 A\right\}}X\left(L\left(v\right)\right)$$
11		2fveq3	$$⊢v=t\to X\left(L\left(v\right)\right)=X\left(L\left(t\right)\right)$$
12	11	cbvsumv	$$⊢\sum _{v\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(v\right)\right)=\sum _{t\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(t\right)\right)$$
13	10 12	syl6eq	$$⊢b=A\to \sum _{v\in \left\{q\in \mathbb{N}|q\parallel b\right\}}X\left(L\left(v\right)\right)=\sum _{t\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(t\right)\right)$$
14		sumex	$$⊢\sum _{t\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(t\right)\right)\in \mathrm{V}$$
15	13 7 14	fvmpt	$$⊢A\in \mathbb{N}\to F\left(A\right)=\sum _{t\in \left\{q\in \mathbb{N}|q\parallel A\right\}}X\left(L\left(t\right)\right)$$