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

Metamath Proof Explorer

Theorem gsummptfzsplitra

Description: Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the right. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummptfzsplita.b ⊢ B = Base G
gsummptfzsplita.p ⊢ + ˙ = + G
gsummptfzsplita.g ⊢ φ → G ∈ CMnd
gsummptfzsplita.n ⊢ φ → N ∈ ℤ ≥ M
gsummptfzsplita.y ⊢ φ ∧ k ∈ M … N → Y ∈ B
gsummptfzsplitra.1 ⊢ φ ∧ k = N → Y = X
Assertion gsummptfzsplitra ⊢ φ → ∑ G k = M N Y = ∑ G k ∈ M ..^ N Y + ˙ X

Proof

Step Hyp Ref Expression
1 gsummptfzsplita.b ⊢ B = Base G
2 gsummptfzsplita.p ⊢ + ˙ = + G
3 gsummptfzsplita.g ⊢ φ → G ∈ CMnd
4 gsummptfzsplita.n ⊢ φ → N ∈ ℤ ≥ M
5 gsummptfzsplita.y ⊢ φ ∧ k ∈ M … N → Y ∈ B
6 gsummptfzsplitra.1 ⊢ φ ∧ k = N → Y = X
7 fzfid ⊢ φ → M … N ∈ Fin
8 fzodisjsn ⊢ M ..^ N ∩ N = ∅
9 8 a1i ⊢ φ → M ..^ N ∩ N = ∅
10 fzisfzounsn ⊢ N ∈ ℤ ≥ M → M … N = M ..^ N ∪ N
11 4 10 syl ⊢ φ → M … N = M ..^ N ∪ N
12 1 2 3 7 5 9 11 gsummptfidmsplit ⊢ φ → ∑ G k = M N Y = ∑ G k ∈ M ..^ N Y + ˙ ∑ G k ∈ N Y
13 3 cmnmndd ⊢ φ → G ∈ Mnd
14 4 6 csbied ⊢ φ → ⦋ N / k⦌ Y = X
15 eluzfz2 ⊢ N ∈ ℤ ≥ M → N ∈ M … N
16 4 15 syl ⊢ φ → N ∈ M … N
17 5 ralrimiva ⊢ φ → ∀ k ∈ M … N Y ∈ B
18 rspcsbela ⊢ N ∈ M … N ∧ ∀ k ∈ M … N Y ∈ B → ⦋ N / k⦌ Y ∈ B
19 16 17 18 syl2anc ⊢ φ → ⦋ N / k⦌ Y ∈ B
20 14 19 eqeltrrd ⊢ φ → X ∈ B
21 1 13 4 20 6 gsumsnd ⊢ φ → ∑ G k ∈ N Y = X
22 21 oveq2d ⊢ φ → ∑ G k ∈ M ..^ N Y + ˙ ∑ G k ∈ N Y = ∑ G k ∈ M ..^ N Y + ˙ X
23 12 22 eqtrd ⊢ φ → ∑ G k = M N Y = ∑ G k ∈ M ..^ N Y + ˙ X