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 ⊢ B = Base G
gsummptnn0fzfv.0 ⊢ 0 ˙ = 0 G
gsummptnn0fzfv.g ⊢ φ → G ∈ CMnd
gsummptnn0fzfv.f ⊢ φ → F ∈ B ℕ 0
gsummptnn0fzfv.s ⊢ φ → S ∈ ℕ 0
gsummptnn0fzfv.u ⊢ φ → ∀ x ∈ ℕ 0 S < x → F ⁡ x = 0 ˙
Assertion gsummptnn0fzfv ⊢ φ → ∑ G k ∈ ℕ 0 F ⁡ k = ∑ G k = 0 S F ⁡ k

Proof

Step Hyp Ref Expression
1 gsummptnn0fzfv.b ⊢ B = Base G
2 gsummptnn0fzfv.0 ⊢ 0 ˙ = 0 G
3 gsummptnn0fzfv.g ⊢ φ → G ∈ CMnd
4 gsummptnn0fzfv.f ⊢ φ → F ∈ B ℕ 0
5 gsummptnn0fzfv.s ⊢ φ → S ∈ ℕ 0
6 gsummptnn0fzfv.u ⊢ φ → ∀ x ∈ ℕ 0 S < x → F ⁡ x = 0 ˙
7 elmapi ⊢ F ∈ B ℕ 0 → F : ℕ 0 ⟶ B
8 ffvelcdm ⊢ F : ℕ 0 ⟶ B ∧ k ∈ ℕ 0 → F ⁡ k ∈ B
9 8 ex ⊢ F : ℕ 0 ⟶ B → k ∈ ℕ 0 → F ⁡ k ∈ B
10 4 7 9 3syl ⊢ φ → k ∈ ℕ 0 → F ⁡ k ∈ B
11 10 ralrimiv ⊢ φ → ∀ k ∈ ℕ 0 F ⁡ k ∈ B
12 breq2 ⊢ x = k → S < x ↔ S < k
13 fveqeq2 ⊢ x = k → F ⁡ x = 0 ˙ ↔ F ⁡ k = 0 ˙
14 12 13 imbi12d ⊢ x = k → S < x → F ⁡ x = 0 ˙ ↔ S < k → F ⁡ k = 0 ˙
15 14 cbvralvw ⊢ ∀ x ∈ ℕ 0 S < x → F ⁡ x = 0 ˙ ↔ ∀ k ∈ ℕ 0 S < k → F ⁡ k = 0 ˙
16 6 15 sylib ⊢ φ → ∀ k ∈ ℕ 0 S < k → F ⁡ k = 0 ˙
17 1 2 3 11 5 16 gsummptnn0fz ⊢ φ → ∑ G k ∈ ℕ 0 F ⁡ k = ∑ G k = 0 S F ⁡ k