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

Metamath Proof Explorer

Theorem gsummptfzsplit

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 AV, 25-Oct-2019)

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

Proof

Step	Hyp	Ref	Expression
1		gsummptfzsplit.b	$⊢ B = {Base}_{G}$
2		gsummptfzsplit.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsummptfzsplit.g	$⊢ φ \to G \in CMnd$
4		gsummptfzsplit.n	$⊢ φ \to N \in ℕ_{0}$
5		gsummptfzsplit.y	$⊢ (φ \land k \in (0 \dots N + 1)) \to Y \in B$
6		fzfid	$⊢ φ \to (0 \dots N + 1) \in Fin$
7		fzp1disj	$⊢ (0 \dots N) \cap \{N + 1\} = \emptyset$
8	7	a1i	$⊢ φ \to (0 \dots N) \cap \{N + 1\} = \emptyset$
9		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
10	4 9	sylib	$⊢ φ \to N \in ℤ_{\geq 0}$
11		fzsuc	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N + 1) = (0 \dots N) \cup \{N + 1\}$
12	10 11	syl	$⊢ φ \to (0 \dots N + 1) = (0 \dots N) \cup \{N + 1\}$
13	1 2 3 6 5 8 12	gsummptfidmsplit	$⊢ φ \to {\sum_{G}}_{k = 0}^{N + 1} Y = ({\sum_{G}}_{k = 0}^{N}, Y) \underset{˙}{+} (\underset{k \in \{N + 1\}}{\sum_{G}}, Y)$