This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ℕ → ( 𝐹 ‘ 𝐴 ) = Σ 𝑡 ∈ { 𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴 } ( 𝑋 ‘ ( 𝐿 ‘ 𝑡 ) ) )