Metamath Proof Explorer


Theorem dchrisum0ff

Description: The function F is a real function. (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 𝐹 = ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) )
dchrisum0f.x ( 𝜑𝑋𝐷 )
dchrisum0flb.r ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
Assertion dchrisum0ff ( 𝜑𝐹 : ℕ ⟶ ℝ )

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 dchrisum0f.x ( 𝜑𝑋𝐷 )
9 dchrisum0flb.r ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
10 fzfid ( ( 𝜑𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
11 dvdsssfz1 ( 𝑛 ∈ ℕ → { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ⊆ ( 1 ... 𝑛 ) )
12 11 adantl ( ( 𝜑𝑛 ∈ ℕ ) → { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ⊆ ( 1 ... 𝑛 ) )
13 10 12 ssfid ( ( 𝜑𝑛 ∈ ℕ ) → { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ∈ Fin )
14 9 ad2antrr ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )
15 3 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
16 eqid ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
17 1 16 2 znzrhfo ( 𝑁 ∈ ℕ0𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
18 fof ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
19 15 17 18 3syl ( 𝜑𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
20 19 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
21 elrabi ( 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } → 𝑚 ∈ ℕ )
22 21 nnzd ( 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } → 𝑚 ∈ ℤ )
23 ffvelrn ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐿𝑚 ) ∈ ( Base ‘ 𝑍 ) )
24 20 22 23 syl2an ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ) → ( 𝐿𝑚 ) ∈ ( Base ‘ 𝑍 ) )
25 14 24 ffvelrnd ( ( ( 𝜑𝑛 ∈ ℕ ) ∧ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ) → ( 𝑋 ‘ ( 𝐿𝑚 ) ) ∈ ℝ )
26 13 25 fsumrecl ( ( 𝜑𝑛 ∈ ℕ ) → Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) ∈ ℝ )
27 breq2 ( 𝑏 = 𝑛 → ( 𝑞𝑏𝑞𝑛 ) )
28 27 rabbidv ( 𝑏 = 𝑛 → { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } = { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } )
29 28 sumeq1d ( 𝑏 = 𝑛 → Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) = Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) )
30 2fveq3 ( 𝑣 = 𝑚 → ( 𝑋 ‘ ( 𝐿𝑣 ) ) = ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
31 30 cbvsumv Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) = Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ( 𝑋 ‘ ( 𝐿𝑚 ) )
32 29 31 eqtrdi ( 𝑏 = 𝑛 → Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) = Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
33 32 cbvmptv ( 𝑏 ∈ ℕ ↦ Σ 𝑣 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑏 } ( 𝑋 ‘ ( 𝐿𝑣 ) ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
34 7 33 eqtri 𝐹 = ( 𝑛 ∈ ℕ ↦ Σ 𝑚 ∈ { 𝑞 ∈ ℕ ∣ 𝑞𝑛 } ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
35 26 34 fmptd ( 𝜑𝐹 : ℕ ⟶ ℝ )