gsumsplit1r

Description: Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in Lang p. 4, first formula. (Contributed by AV, 26-Dec-2023)

	Ref	Expression
Hypotheses	gsumsplit1r.b	$⊢ B = {Base}_{G}$
	gsumsplit1r.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumsplit1r.g	$⊢ φ \to G \in V$
	gsumsplit1r.m	$⊢ φ \to M \in ℤ$
	gsumsplit1r.n	$⊢ φ \to N \in ℤ_{\geq M}$
	gsumsplit1r.f	$⊢ φ \to F : (M \dots N + 1) ⟶ B$
Assertion	gsumsplit1r	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{(M \dots N)})) \underset{˙}{+} F (N + 1)$

Proof

Step	Hyp	Ref	Expression
1		gsumsplit1r.b	$⊢ B = {Base}_{G}$
2		gsumsplit1r.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsumsplit1r.g	$⊢ φ \to G \in V$
4		gsumsplit1r.m	$⊢ φ \to M \in ℤ$
5		gsumsplit1r.n	$⊢ φ \to N \in ℤ_{\geq M}$
6		gsumsplit1r.f	$⊢ φ \to F : (M \dots N + 1) ⟶ B$
7		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
8	5 7	syl	$⊢ φ \to N + 1 \in ℤ_{\geq M}$
9	1 2 3 8 6	gsumval2	$⊢ φ \to \sum_{G} F = seq M (\underset{˙}{+}, F) (N + 1)$
10		seqp1	$⊢ N \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (N + 1) = seq M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N + 1)$
11	5 10	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) (N + 1) = seq M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N + 1)$
12		fzssp1	$⊢ (M \dots N) \subseteq (M \dots N + 1)$
13	12	a1i	$⊢ φ \to (M \dots N) \subseteq (M \dots N + 1)$
14	6 13	fssresd	$⊢ φ \to ({F ↾}_{(M \dots N)}) : (M \dots N) ⟶ B$
15	1 2 3 5 14	gsumval2	$⊢ φ \to \sum_{G} ({F ↾}_{(M \dots N)}) = seq M (\underset{˙}{+}, ({F ↾}_{(M \dots N)})) (N)$
16	4	uzidd	$⊢ φ \to M \in ℤ_{\geq M}$
17		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, ({F ↾}_{(M \dots N)})) (M) = ({F ↾}_{(M \dots N)}) (M)$
18	4 17	syl	$⊢ φ \to seq M (\underset{˙}{+}, ({F ↾}_{(M \dots N)})) (M) = ({F ↾}_{(M \dots N)}) (M)$
19		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
20	5 19	syl	$⊢ φ \to M \in (M \dots N)$
21	20	fvresd	$⊢ φ \to ({F ↾}_{(M \dots N)}) (M) = F (M)$
22	18 21	eqtrd	$⊢ φ \to seq M (\underset{˙}{+}, ({F ↾}_{(M \dots N)})) (M) = F (M)$
23		fzp1ss	$⊢ M \in ℤ \to (M + 1 \dots N) \subseteq (M \dots N)$
24	4 23	syl	$⊢ φ \to (M + 1 \dots N) \subseteq (M \dots N)$
25	24	sselda	$⊢ (φ \land x \in (M + 1 \dots N)) \to x \in (M \dots N)$
26	25	fvresd	$⊢ (φ \land x \in (M + 1 \dots N)) \to ({F ↾}_{(M \dots N)}) (x) = F (x)$
27	16 22 5 26	seqfveq2	$⊢ φ \to seq M (\underset{˙}{+}, ({F ↾}_{(M \dots N)})) (N) = seq M (\underset{˙}{+}, F) (N)$
28	15 27	eqtr2d	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = \sum_{G} ({F ↾}_{(M \dots N)})$
29	28	oveq1d	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) \underset{˙}{+} F (N + 1) = (\sum_{G}, ({F ↾}_{(M \dots N)})) \underset{˙}{+} F (N + 1)$
30	9 11 29	3eqtrd	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{(M \dots N)})) \underset{˙}{+} F (N + 1)$

Metamath Proof Explorer

Theorem gsumsplit1r

Proof