gsummptfzsplitl

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 AV, 7-Nov-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}$
	gsummptfzsplitl.y	$⊢ (φ \land k \in (0 \dots N)) \to Y \in B$
Assertion	gsummptfzsplitl	$⊢ φ \to {\sum_{G}}_{k = 0}^{N} Y = ({\sum_{G}}_{k = 1}^{N}, Y) \underset{˙}{+} (\underset{k \in \{0\}}{\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		gsummptfzsplitl.y	$⊢ (φ \land k \in (0 \dots N)) \to Y \in B$
6		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
7		incom	$⊢ (1 \dots N) \cap \{0\} = \{0\} \cap (1 \dots N)$
8	7	a1i	$⊢ φ \to (1 \dots N) \cap \{0\} = \{0\} \cap (1 \dots N)$
9		1e0p1	$⊢ 1 = 0 + 1$
10	9	oveq1i	$⊢ (1 \dots N) = (0 + 1 \dots N)$
11	10	a1i	$⊢ φ \to (1 \dots N) = (0 + 1 \dots N)$
12	11	ineq2d	$⊢ φ \to \{0\} \cap (1 \dots N) = \{0\} \cap (0 + 1 \dots N)$
13		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
14	13	biimpi	$⊢ N \in ℕ_{0} \to N \in ℤ_{\geq 0}$
15		fzpreddisj	$⊢ N \in ℤ_{\geq 0} \to \{0\} \cap (0 + 1 \dots N) = \emptyset$
16	4 14 15	3syl	$⊢ φ \to \{0\} \cap (0 + 1 \dots N) = \emptyset$
17	8 12 16	3eqtrd	$⊢ φ \to (1 \dots N) \cap \{0\} = \emptyset$
18		fzpred	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
19	4 14 18	3syl	$⊢ φ \to (0 \dots N) = \{0\} \cup (0 + 1 \dots N)$
20		uncom	$⊢ \{0\} \cup (0 + 1 \dots N) = (0 + 1 \dots N) \cup \{0\}$
21		0p1e1	$⊢ 0 + 1 = 1$
22	21	oveq1i	$⊢ (0 + 1 \dots N) = (1 \dots N)$
23	22	uneq1i	$⊢ (0 + 1 \dots N) \cup \{0\} = (1 \dots N) \cup \{0\}$
24	20 23	eqtri	$⊢ \{0\} \cup (0 + 1 \dots N) = (1 \dots N) \cup \{0\}$
25	19 24	eqtrdi	$⊢ φ \to (0 \dots N) = (1 \dots N) \cup \{0\}$
26	1 2 3 6 5 17 25	gsummptfidmsplit	$⊢ φ \to {\sum_{G}}_{k = 0}^{N} Y = ({\sum_{G}}_{k = 1}^{N}, Y) \underset{˙}{+} (\underset{k \in \{0\}}{\sum_{G}}, Y)$

Metamath Proof Explorer

Theorem gsummptfzsplitl

Proof