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

Metamath Proof Explorer

Theorem gsummptnn0fzfv

Description: A final group sum over a function over the nonnegative integers (given as mapping to its function values) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019)

Ref Expression
Hypotheses gsummptnn0fzfv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptnn0fzfv.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsummptnn0fzfv.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptnn0fzfv.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
gsummptnn0fzfv.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
gsummptnn0fzfv.u ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
Assertion gsummptnn0fzfv ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummptnn0fzfv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptnn0fzfv.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsummptnn0fzfv.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptnn0fzfv.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
5 gsummptnn0fzfv.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
6 gsummptnn0fzfv.u ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
7 elmapi ⊢ ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) → 𝐹 : ℕ0 ⟶ 𝐵 )
8 ffvelcdm ⊢ ( ( 𝐹 : ℕ0 ⟶ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
9 8 ex ⊢ ( 𝐹 : ℕ0 ⟶ 𝐵 → ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
10 4 7 9 3syl ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ) )
11 10 ralrimiv ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
12 breq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑆 < 𝑥 ↔ 𝑆 < 𝑘 ) )
13 fveqeq2 ⊢ ( 𝑥 = 𝑘 → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ 𝑘 ) = 0 ) )
14 12 13 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ↔ ( 𝑆 < 𝑘 → ( 𝐹 ‘ 𝑘 ) = 0 ) ) )
15 14 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → ( 𝐹 ‘ 𝑘 ) = 0 ) )
16 6 15 sylib ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝑆 < 𝑘 → ( 𝐹 ‘ 𝑘 ) = 0 ) )
17 1 2 3 11 5 16 gsummptnn0fz ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 0 ... 𝑆 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )