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	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum2.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
Assertion	dchrisum0fval	⊢ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐴 ) = Σ 𝑡 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑡 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum2.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum2.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum2.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum0f.f	⊢ 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
8		breq2	⊢ ( 𝑏 = 𝐴 → ( 𝑞 ∥ 𝑏 ↔ 𝑞 ∥ 𝐴 ) )
9	8	rabbidv	⊢ ( 𝑏 = 𝐴 → { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } = { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } )
10	9	sumeq1d	⊢ ( 𝑏 = 𝐴 → Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) )
11		2fveq3	⊢ ( 𝑣 = 𝑡 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑡 ) ) )
12	11	cbvsumv	⊢ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = Σ 𝑡 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑡 ) )
13	10 12	eqtrdi	⊢ ( 𝑏 = 𝐴 → Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑣 ) ) = Σ 𝑡 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑡 ) ) )
14		sumex	⊢ Σ 𝑡 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑡 ) ) ∈ V
15	13 7 14	fvmpt	⊢ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐴 ) = Σ 𝑡 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑡 ) ) )