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