gsummptfzsplitla

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 left. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	gsummptfzsplita.b	$⊢ B = {Base}_{G}$
	gsummptfzsplita.p	$⊢ \underset{˙}{+} = +_{G}$
	gsummptfzsplita.g	$⊢ φ \to G \in CMnd$
	gsummptfzsplita.n	$⊢ φ \to N \in ℤ_{\geq M}$
	gsummptfzsplita.y	$⊢ (φ \land k \in (M \dots N)) \to Y \in B$
	gsummptfzsplitla.1	$⊢ (φ \land k = M) \to Y = X$
Assertion	gsummptfzsplitla	$⊢ φ \to {\sum_{G}}_{k = M}^{N} Y = X \underset{˙}{+} ({\sum_{G}}_{k = M + 1}^{N}, Y)$

Proof

Step	Hyp	Ref	Expression
1		gsummptfzsplita.b	$⊢ B = {Base}_{G}$
2		gsummptfzsplita.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsummptfzsplita.g	$⊢ φ \to G \in CMnd$
4		gsummptfzsplita.n	$⊢ φ \to N \in ℤ_{\geq M}$
5		gsummptfzsplita.y	$⊢ (φ \land k \in (M \dots N)) \to Y \in B$
6		gsummptfzsplitla.1	$⊢ (φ \land k = M) \to Y = X$
7		fzfid	$⊢ φ \to (M \dots N) \in Fin$
8		fzpreddisj	$⊢ N \in ℤ_{\geq M} \to \{M\} \cap (M + 1 \dots N) = \emptyset$
9	4 8	syl	$⊢ φ \to \{M\} \cap (M + 1 \dots N) = \emptyset$
10		fzpred	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
11	4 10	syl	$⊢ φ \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
12	1 2 3 7 5 9 11	gsummptfidmsplit	$⊢ φ \to {\sum_{G}}_{k = M}^{N} Y = (\underset{k \in \{M\}}{\sum_{G}}, Y) \underset{˙}{+} ({\sum_{G}}_{k = M + 1}^{N}, Y)$
13	3	cmnmndd	$⊢ φ \to G \in Mnd$
14	4	elfvexd	$⊢ φ \to M \in V$
15	14 6	csbied	$⊢ φ \to ⦋ M / k ⦌ Y = X$
16		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
17	4 16	syl	$⊢ φ \to M \in (M \dots N)$
18	5	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) Y \in B$
19		rspcsbela	$⊢ (M \in (M \dots N) \land \forall k \in (M \dots N) Y \in B) \to ⦋ M / k ⦌ Y \in B$
20	17 18 19	syl2anc	$⊢ φ \to ⦋ M / k ⦌ Y \in B$
21	15 20	eqeltrrd	$⊢ φ \to X \in B$
22	1 13 14 21 6	gsumsnd	$⊢ φ \to \underset{k \in \{M\}}{\sum_{G}} Y = X$
23	22	oveq1d	$⊢ φ \to (\underset{k \in \{M\}}{\sum_{G}}, Y) \underset{˙}{+} ({\sum_{G}}_{k = M + 1}^{N}, Y) = X \underset{˙}{+} ({\sum_{G}}_{k = M + 1}^{N}, Y)$
24	12 23	eqtrd	$⊢ φ \to {\sum_{G}}_{k = M}^{N} Y = X \underset{˙}{+} ({\sum_{G}}_{k = M + 1}^{N}, Y)$

Metamath Proof Explorer

Theorem gsummptfzsplitla

Proof