gsumnunsn

Description: Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018)

	Ref	Expression
Hypotheses	gsumncl.k	$⊢ K = {Base}_{M}$
	gsumncl.w	$⊢ φ \to M \in Mnd$
	gsumncl.p	$⊢ φ \to P \in ℤ_{\geq N}$
	gsumncl.b	$⊢ (φ \land k \in (N \dots P)) \to B \in K$
	gsumnunsn.a	$⊢ \underset{˙}{+} = +_{M}$
	gsumnunsn.l	$⊢ φ \to C \in K$
	gsumnunsn.c	$⊢ (φ \land k = P + 1) \to B = C$
Assertion	gsumnunsn	$⊢ φ \to {\sum_{M}}_{k = N}^{P + 1} B = ({\sum_{M}}_{k = N}^{P}, B) \underset{˙}{+} C$

Proof

Step	Hyp	Ref	Expression
1		gsumncl.k	$⊢ K = {Base}_{M}$
2		gsumncl.w	$⊢ φ \to M \in Mnd$
3		gsumncl.p	$⊢ φ \to P \in ℤ_{\geq N}$
4		gsumncl.b	$⊢ (φ \land k \in (N \dots P)) \to B \in K$
5		gsumnunsn.a	$⊢ \underset{˙}{+} = +_{M}$
6		gsumnunsn.l	$⊢ φ \to C \in K$
7		gsumnunsn.c	$⊢ (φ \land k = P + 1) \to B = C$
8		seqp1	$⊢ P \in ℤ_{\geq N} \to seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P + 1) = seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P) \underset{˙}{+} (k \in (N \dots P + 1) ⟼ B) (P + 1)$
9	3 8	syl	$⊢ φ \to seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P + 1) = seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P) \underset{˙}{+} (k \in (N \dots P + 1) ⟼ B) (P + 1)$
10		peano2uz	$⊢ P \in ℤ_{\geq N} \to P + 1 \in ℤ_{\geq N}$
11	3 10	syl	$⊢ φ \to P + 1 \in ℤ_{\geq N}$
12	4	adantlr	$⊢ ((φ \land k \in (N \dots P + 1)) \land k \in (N \dots P)) \to B \in K$
13	7	adantlr	$⊢ ((φ \land k \in (N \dots P + 1)) \land k = P + 1) \to B = C$
14	6	ad2antrr	$⊢ ((φ \land k \in (N \dots P + 1)) \land k = P + 1) \to C \in K$
15	13 14	eqeltrd	$⊢ ((φ \land k \in (N \dots P + 1)) \land k = P + 1) \to B \in K$
16		elfzp1	$⊢ P \in ℤ_{\geq N} \to (k \in (N \dots P + 1) \leftrightarrow (k \in (N \dots P) \lor k = P + 1))$
17	3 16	syl	$⊢ φ \to (k \in (N \dots P + 1) \leftrightarrow (k \in (N \dots P) \lor k = P + 1))$
18	17	biimpa	$⊢ (φ \land k \in (N \dots P + 1)) \to (k \in (N \dots P) \lor k = P + 1)$
19	12 15 18	mpjaodan	$⊢ (φ \land k \in (N \dots P + 1)) \to B \in K$
20	19	fmpttd	$⊢ φ \to (k \in (N \dots P + 1) ⟼ B) : (N \dots P + 1) ⟶ K$
21	1 5 2 11 20	gsumval2	$⊢ φ \to {\sum_{M}}_{k = N}^{P + 1} B = seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P + 1)$
22	4	fmpttd	$⊢ φ \to (k \in (N \dots P) ⟼ B) : (N \dots P) ⟶ K$
23	1 5 2 3 22	gsumval2	$⊢ φ \to {\sum_{M}}_{k = N}^{P} B = seq N (\underset{˙}{+}, (k \in (N \dots P) ⟼ B)) (P)$
24		fvres	$⊢ i \in (N \dots P) \to ({(k \in (N \dots P + 1) ⟼ B) ↾}_{(N \dots P)}) (i) = (k \in (N \dots P + 1) ⟼ B) (i)$
25	24	adantl	$⊢ (φ \land i \in (N \dots P)) \to ({(k \in (N \dots P + 1) ⟼ B) ↾}_{(N \dots P)}) (i) = (k \in (N \dots P + 1) ⟼ B) (i)$
26		fzssp1	$⊢ (N \dots P) \subseteq (N \dots P + 1)$
27		resmpt	$⊢ (N \dots P) \subseteq (N \dots P + 1) \to {(k \in (N \dots P + 1) ⟼ B) ↾}_{(N \dots P)} = (k \in (N \dots P) ⟼ B)$
28	26 27	ax-mp	$⊢ {(k \in (N \dots P + 1) ⟼ B) ↾}_{(N \dots P)} = (k \in (N \dots P) ⟼ B)$
29	28	fveq1i	$⊢ ({(k \in (N \dots P + 1) ⟼ B) ↾}_{(N \dots P)}) (i) = (k \in (N \dots P) ⟼ B) (i)$
30	25 29	eqtr3di	$⊢ (φ \land i \in (N \dots P)) \to (k \in (N \dots P + 1) ⟼ B) (i) = (k \in (N \dots P) ⟼ B) (i)$
31	3 30	seqfveq	$⊢ φ \to seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P) = seq N (\underset{˙}{+}, (k \in (N \dots P) ⟼ B)) (P)$
32	23 31	eqtr4d	$⊢ φ \to {\sum_{M}}_{k = N}^{P} B = seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P)$
33		eqidd	$⊢ φ \to (k \in (N \dots P + 1) ⟼ B) = (k \in (N \dots P + 1) ⟼ B)$
34		eluzfz2	$⊢ P + 1 \in ℤ_{\geq N} \to P + 1 \in (N \dots P + 1)$
35	11 34	syl	$⊢ φ \to P + 1 \in (N \dots P + 1)$
36	33 7 35 6	fvmptd	$⊢ φ \to (k \in (N \dots P + 1) ⟼ B) (P + 1) = C$
37	36	eqcomd	$⊢ φ \to C = (k \in (N \dots P + 1) ⟼ B) (P + 1)$
38	32 37	oveq12d	$⊢ φ \to ({\sum_{M}}_{k = N}^{P}, B) \underset{˙}{+} C = seq N (\underset{˙}{+}, (k \in (N \dots P + 1) ⟼ B)) (P) \underset{˙}{+} (k \in (N \dots P + 1) ⟼ B) (P + 1)$
39	9 21 38	3eqtr4d	$⊢ φ \to {\sum_{M}}_{k = N}^{P + 1} B = ({\sum_{M}}_{k = N}^{P}, B) \underset{˙}{+} C$

Metamath Proof Explorer

Theorem gsumnunsn

Proof