gsummulsubdishift1

Description: Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	gsummulsubdishift.b	$⊢ B = {Base}_{R}$
	gsummulsubdishift.p	$⊢ \underset{˙}{+} = +_{R}$
	gsummulsubdishift.m	$⊢ \underset{˙}{-} = -_{R}$
	gsummulsubdishift.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	gsummulsubdishift.r	$⊢ φ \to R \in Ring$
	gsummulsubdishift.a	$⊢ φ \to A \in B$
	gsummulsubdishift.c	$⊢ φ \to C \in B$
	gsummulsubdishift.n	$⊢ φ \to N \in ℕ_{0}$
	gsummulsubdishift.d	$⊢ φ \to D : (0 \dots N) ⟶ B$
	gsummulsubdishift1.e	$⊢ φ \to E = (D (N) \underset{˙}{\cdot} A) \underset{˙}{-} (D (0) \underset{˙}{\cdot} C)$
	gsummulsubdishift1.f	$⊢ (φ \land k \in (0 ..^N)) \to F = (D (k) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} C)$
Assertion	gsummulsubdishift1	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} (A \underset{˙}{-} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$

Proof

Step	Hyp	Ref	Expression
1		gsummulsubdishift.b	$⊢ B = {Base}_{R}$
2		gsummulsubdishift.p	$⊢ \underset{˙}{+} = +_{R}$
3		gsummulsubdishift.m	$⊢ \underset{˙}{-} = -_{R}$
4		gsummulsubdishift.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		gsummulsubdishift.r	$⊢ φ \to R \in Ring$
6		gsummulsubdishift.a	$⊢ φ \to A \in B$
7		gsummulsubdishift.c	$⊢ φ \to C \in B$
8		gsummulsubdishift.n	$⊢ φ \to N \in ℕ_{0}$
9		gsummulsubdishift.d	$⊢ φ \to D : (0 \dots N) ⟶ B$
10		gsummulsubdishift1.e	$⊢ φ \to E = (D (N) \underset{˙}{\cdot} A) \underset{˙}{-} (D (0) \underset{˙}{\cdot} C)$
11		gsummulsubdishift1.f	$⊢ (φ \land k \in (0 ..^N)) \to F = (D (k) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} C)$
12	5	ringcmnd	$⊢ φ \to R \in CMnd$
13		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
14	9	ffvelcdmda	$⊢ (φ \land k \in (0 \dots N)) \to D (k) \in B$
15	14	ralrimiva	$⊢ φ \to \forall k \in (0 \dots N) D (k) \in B$
16	1 12 13 15	gsummptcl	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} D (k) \in B$
17	1 4 3 5 16 6 7	ringsubdi	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} (A \underset{˙}{-} C) = (({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} A) \underset{˙}{-} (({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} C)$
18		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
19	8 18	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
20		fzisfzounsn	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N) = (0 ..^N) \cup \{N\}$
21	19 20	syl	$⊢ φ \to (0 \dots N) = (0 ..^N) \cup \{N\}$
22	21	mpteq1d	$⊢ φ \to (k \in (0 \dots N) ⟼ D (k) \underset{˙}{\cdot} A) = (k \in ((0 ..^N) \cup \{N\}) ⟼ D (k) \underset{˙}{\cdot} A)$
23	22	oveq2d	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (D (k) \underset{˙}{\cdot} A) = \underset{k \in (0 ..^N) \cup \{N\}}{\sum_{R}} (D (k) \underset{˙}{\cdot} A)$
24		eqid	$⊢ 0_{R} = 0_{R}$
25		eqid	$⊢ (k \in (0 \dots N) ⟼ D (k)) = (k \in (0 \dots N) ⟼ D (k))$
26		fvexd	$⊢ φ \to 0_{R} \in V$
27	25 13 14 26	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{R}} ((k \in (0 \dots N) ⟼ D (k)))$
28	1 24 4 5 13 6 14 27	gsummulc1	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (D (k) \underset{˙}{\cdot} A) = ({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} A$
29		fzofi	$⊢ (0 ..^N) \in Fin$
30	29	a1i	$⊢ φ \to (0 ..^N) \in Fin$
31	5	adantr	$⊢ (φ \land k \in (0 ..^N)) \to R \in Ring$
32		fzossfz	$⊢ (0 ..^N) \subseteq (0 \dots N)$
33	32	a1i	$⊢ φ \to (0 ..^N) \subseteq (0 \dots N)$
34	33	sselda	$⊢ (φ \land k \in (0 ..^N)) \to k \in (0 \dots N)$
35	34 14	syldan	$⊢ (φ \land k \in (0 ..^N)) \to D (k) \in B$
36	6	adantr	$⊢ (φ \land k \in (0 ..^N)) \to A \in B$
37	1 4 31 35 36	ringcld	$⊢ (φ \land k \in (0 ..^N)) \to D (k) \underset{˙}{\cdot} A \in B$
38		fzonel	$⊢ \neg N \in (0 ..^N)$
39	38	a1i	$⊢ φ \to \neg N \in (0 ..^N)$
40		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
41	8 40	sylib	$⊢ φ \to N \in (0 \dots N)$
42	9 41	ffvelcdmd	$⊢ φ \to D (N) \in B$
43	1 4 5 42 6	ringcld	$⊢ φ \to D (N) \underset{˙}{\cdot} A \in B$
44		fveq2	$⊢ k = N \to D (k) = D (N)$
45	44	oveq1d	$⊢ k = N \to D (k) \underset{˙}{\cdot} A = D (N) \underset{˙}{\cdot} A$
46	1 2 12 30 37 8 39 43 45	gsumunsn	$⊢ φ \to \underset{k \in (0 ..^N) \cup \{N\}}{\sum_{R}} (D (k) \underset{˙}{\cdot} A) = (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{+} (D (N) \underset{˙}{\cdot} A)$
47	23 28 46	3eqtr3d	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} A = (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{+} (D (N) \underset{˙}{\cdot} A)$
48	1 24 4 5 13 7 14 27	gsummulc1	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (D (k) \underset{˙}{\cdot} C) = ({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} C$
49		fz0sn0fz1	$⊢ N \in ℕ_{0} \to (0 \dots N) = \{0\} \cup (1 \dots N)$
50	8 49	syl	$⊢ φ \to (0 \dots N) = \{0\} \cup (1 \dots N)$
51		uncom	$⊢ (1 \dots N) \cup \{0\} = \{0\} \cup (1 \dots N)$
52	50 51	eqtr4di	$⊢ φ \to (0 \dots N) = (1 \dots N) \cup \{0\}$
53	52	mpteq1d	$⊢ φ \to (k \in (0 \dots N) ⟼ D (k) \underset{˙}{\cdot} C) = (k \in ((1 \dots N) \cup \{0\}) ⟼ D (k) \underset{˙}{\cdot} C)$
54	53	oveq2d	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (D (k) \underset{˙}{\cdot} C) = \underset{k \in (1 \dots N) \cup \{0\}}{\sum_{R}} (D (k) \underset{˙}{\cdot} C)$
55		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
56	5	adantr	$⊢ (φ \land k \in (1 \dots N)) \to R \in Ring$
57		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
58	57	a1i	$⊢ φ \to (1 \dots N) \subseteq (0 \dots N)$
59	58	sselda	$⊢ (φ \land k \in (1 \dots N)) \to k \in (0 \dots N)$
60	59 14	syldan	$⊢ (φ \land k \in (1 \dots N)) \to D (k) \in B$
61	7	adantr	$⊢ (φ \land k \in (1 \dots N)) \to C \in B$
62	1 4 56 60 61	ringcld	$⊢ (φ \land k \in (1 \dots N)) \to D (k) \underset{˙}{\cdot} C \in B$
63		c0ex	$⊢ 0 \in V$
64	63	a1i	$⊢ φ \to 0 \in V$
65		0nnn	$⊢ \neg 0 \in ℕ$
66		elfznn	$⊢ 0 \in (1 \dots N) \to 0 \in ℕ$
67	65 66	mto	$⊢ \neg 0 \in (1 \dots N)$
68	67	a1i	$⊢ φ \to \neg 0 \in (1 \dots N)$
69		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
70	8 69	syl	$⊢ φ \to 0 \in (0 \dots N)$
71	9 70	ffvelcdmd	$⊢ φ \to D (0) \in B$
72	1 4 5 71 7	ringcld	$⊢ φ \to D (0) \underset{˙}{\cdot} C \in B$
73		fveq2	$⊢ k = 0 \to D (k) = D (0)$
74	73	oveq1d	$⊢ k = 0 \to D (k) \underset{˙}{\cdot} C = D (0) \underset{˙}{\cdot} C$
75	1 2 12 55 62 64 68 72 74	gsumunsn	$⊢ φ \to \underset{k \in (1 \dots N) \cup \{0\}}{\sum_{R}} (D (k) \underset{˙}{\cdot} C) = ({\sum_{R}}_{k = 1}^{N}, (D (k) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C)$
76		nfcv	$⊢ \underline{Ⅎ} k (D (l + 1) \underset{˙}{\cdot} C)$
77		fveq2	$⊢ k = l + 1 \to D (k) = D (l + 1)$
78	77	oveq1d	$⊢ k = l + 1 \to D (k) \underset{˙}{\cdot} C = D (l + 1) \underset{˙}{\cdot} C$
79		ssidd	$⊢ φ \to B \subseteq B$
80	8	nn0zd	$⊢ φ \to N \in ℤ$
81		fzoval	$⊢ N \in ℤ \to (0 ..^N) = (0 \dots N - 1)$
82	80 81	syl	$⊢ φ \to (0 ..^N) = (0 \dots N - 1)$
83	82	eleq2d	$⊢ φ \to (l \in (0 ..^N) \leftrightarrow l \in (0 \dots N - 1))$
84	83	biimpar	$⊢ (φ \land l \in (0 \dots N - 1)) \to l \in (0 ..^N)$
85		fz0add1fz1	$⊢ (N \in ℕ_{0} \land l \in (0 ..^N)) \to l + 1 \in (1 \dots N)$
86	8 84 85	syl2an2r	$⊢ (φ \land l \in (0 \dots N - 1)) \to l + 1 \in (1 \dots N)$
87	59	elfzelzd	$⊢ (φ \land k \in (1 \dots N)) \to k \in ℤ$
88	80	adantr	$⊢ (φ \land k \in (1 \dots N)) \to N \in ℤ$
89		simpr	$⊢ (φ \land k \in (1 \dots N)) \to k \in (1 \dots N)$
90		elfzm1b	$⊢ (k \in ℤ \land N \in ℤ) \to (k \in (1 \dots N) \leftrightarrow k - 1 \in (0 \dots N - 1))$
91	90	biimpa	$⊢ ((k \in ℤ \land N \in ℤ) \land k \in (1 \dots N)) \to k - 1 \in (0 \dots N - 1)$
92	87 88 89 91	syl21anc	$⊢ (φ \land k \in (1 \dots N)) \to k - 1 \in (0 \dots N - 1)$
93		eqcom	$⊢ l + 1 = k \leftrightarrow k = l + 1$
94		elfznn0	$⊢ l \in (0 \dots N - 1) \to l \in ℕ_{0}$
95	94	nn0cnd	$⊢ l \in (0 \dots N - 1) \to l \in ℂ$
96	95	adantl	$⊢ ((φ \land k \in (1 \dots N)) \land l \in (0 \dots N - 1)) \to l \in ℂ$
97		1cnd	$⊢ ((φ \land k \in (1 \dots N)) \land l \in (0 \dots N - 1)) \to 1 \in ℂ$
98	87	zcnd	$⊢ (φ \land k \in (1 \dots N)) \to k \in ℂ$
99	98	adantr	$⊢ ((φ \land k \in (1 \dots N)) \land l \in (0 \dots N - 1)) \to k \in ℂ$
100	96 97 99	addlsub	$⊢ ((φ \land k \in (1 \dots N)) \land l \in (0 \dots N - 1)) \to (l + 1 = k \leftrightarrow l = k - 1)$
101	93 100	bitr3id	$⊢ ((φ \land k \in (1 \dots N)) \land l \in (0 \dots N - 1)) \to (k = l + 1 \leftrightarrow l = k - 1)$
102	92 101	reu6dv	$⊢ (φ \land k \in (1 \dots N)) \to \exists! l \in (0 \dots N - 1) k = l + 1$
103	76 1 24 78 12 55 79 62 86 102	gsummptf1o	$⊢ φ \to {\sum_{R}}_{k = 1}^{N} (D (k) \underset{˙}{\cdot} C) = {\sum_{R}}_{l = 0}^{N - 1} (D (l + 1) \underset{˙}{\cdot} C)$
104		fvoveq1	$⊢ l = k \to D (l + 1) = D (k + 1)$
105	104	oveq1d	$⊢ l = k \to D (l + 1) \underset{˙}{\cdot} C = D (k + 1) \underset{˙}{\cdot} C$
106	105	cbvmptv	$⊢ (l \in (0 \dots N - 1) ⟼ D (l + 1) \underset{˙}{\cdot} C) = (k \in (0 \dots N - 1) ⟼ D (k + 1) \underset{˙}{\cdot} C)$
107	82	mpteq1d	$⊢ φ \to (k \in (0 ..^N) ⟼ D (k + 1) \underset{˙}{\cdot} C) = (k \in (0 \dots N - 1) ⟼ D (k + 1) \underset{˙}{\cdot} C)$
108	106 107	eqtr4id	$⊢ φ \to (l \in (0 \dots N - 1) ⟼ D (l + 1) \underset{˙}{\cdot} C) = (k \in (0 ..^N) ⟼ D (k + 1) \underset{˙}{\cdot} C)$
109	108	oveq2d	$⊢ φ \to {\sum_{R}}_{l = 0}^{N - 1} (D (l + 1) \underset{˙}{\cdot} C) = \underset{k \in (0 ..^N)}{\sum_{R}} (D (k + 1) \underset{˙}{\cdot} C)$
110	103 109	eqtrd	$⊢ φ \to {\sum_{R}}_{k = 1}^{N} (D (k) \underset{˙}{\cdot} C) = \underset{k \in (0 ..^N)}{\sum_{R}} (D (k + 1) \underset{˙}{\cdot} C)$
111	110	oveq1d	$⊢ φ \to ({\sum_{R}}_{k = 1}^{N}, (D (k) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C)$
112	54 75 111	3eqtrd	$⊢ φ \to {\sum_{R}}_{k = 0}^{N} (D (k) \underset{˙}{\cdot} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C)$
113	48 112	eqtr3d	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} C = (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C)$
114	47 113	oveq12d	$⊢ φ \to (({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} A) \underset{˙}{-} (({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} C) = ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{+} (D (N) \underset{˙}{\cdot} A)) \underset{˙}{-} ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C))$
115	5	ringabld	$⊢ φ \to R \in Abel$
116	37	ralrimiva	$⊢ φ \to \forall k \in (0 ..^N) D (k) \underset{˙}{\cdot} A \in B$
117	1 12 30 116	gsummptcl	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} (D (k) \underset{˙}{\cdot} A) \in B$
118	9	adantr	$⊢ (φ \land k \in (0 ..^N)) \to D : (0 \dots N) ⟶ B$
119		fz0add1fz1	$⊢ (N \in ℕ_{0} \land k \in (0 ..^N)) \to k + 1 \in (1 \dots N)$
120	8 119	sylan	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \in (1 \dots N)$
121	57 120	sselid	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \in (0 \dots N)$
122	118 121	ffvelcdmd	$⊢ (φ \land k \in (0 ..^N)) \to D (k + 1) \in B$
123	7	adantr	$⊢ (φ \land k \in (0 ..^N)) \to C \in B$
124	1 4 31 122 123	ringcld	$⊢ (φ \land k \in (0 ..^N)) \to D (k + 1) \underset{˙}{\cdot} C \in B$
125	124	ralrimiva	$⊢ φ \to \forall k \in (0 ..^N) D (k + 1) \underset{˙}{\cdot} C \in B$
126	1 12 30 125	gsummptcl	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} (D (k + 1) \underset{˙}{\cdot} C) \in B$
127	1 2 3	ablsub4	$⊢ (R \in Abel \land (\underset{k \in (0 ..^N)}{\sum_{R}} (D (k) \underset{˙}{\cdot} A) \in B \land D (N) \underset{˙}{\cdot} A \in B) \land (\underset{k \in (0 ..^N)}{\sum_{R}} (D (k + 1) \underset{˙}{\cdot} C) \in B \land D (0) \underset{˙}{\cdot} C \in B)) \to ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{+} (D (N) \underset{˙}{\cdot} A)) \underset{˙}{-} ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C)) = ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{-} (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C))) \underset{˙}{+} ((D (N) \underset{˙}{\cdot} A) \underset{˙}{-} (D (0) \underset{˙}{\cdot} C))$
128	115 117 43 126 72 127	syl122anc	$⊢ φ \to ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{+} (D (N) \underset{˙}{\cdot} A)) \underset{˙}{-} ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C)) \underset{˙}{+} (D (0) \underset{˙}{\cdot} C)) = ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{-} (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C))) \underset{˙}{+} ((D (N) \underset{˙}{\cdot} A) \underset{˙}{-} (D (0) \underset{˙}{\cdot} C))$
129	17 114 128	3eqtrd	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} (A \underset{˙}{-} C) = ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{-} (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C))) \underset{˙}{+} ((D (N) \underset{˙}{\cdot} A) \underset{˙}{-} (D (0) \underset{˙}{\cdot} C))$
130	9	feqmptd	$⊢ φ \to D = (k \in (0 \dots N) ⟼ D (k))$
131	130	oveq2d	$⊢ φ \to \sum_{R} D = {\sum_{R}}_{k = 0}^{N} D (k)$
132	131	oveq1d	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} (A \underset{˙}{-} C) = ({\sum_{R}}_{k = 0}^{N}, D (k)) \underset{˙}{\cdot} (A \underset{˙}{-} C)$
133	11	mpteq2dva	$⊢ φ \to (k \in (0 ..^N) ⟼ F) = (k \in (0 ..^N) ⟼ (D (k) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} C))$
134	133	oveq2d	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} F = \underset{k \in (0 ..^N)}{\sum_{R}} ((D (k) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} C))$
135		eqid	$⊢ (k \in (0 ..^N) ⟼ D (k) \underset{˙}{\cdot} A) = (k \in (0 ..^N) ⟼ D (k) \underset{˙}{\cdot} A)$
136		eqid	$⊢ (k \in (0 ..^N) ⟼ D (k + 1) \underset{˙}{\cdot} C) = (k \in (0 ..^N) ⟼ D (k + 1) \underset{˙}{\cdot} C)$
137	1 3 115 30 37 124 135 136	gsummptfidmsub	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} ((D (k) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} C)) = (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{-} (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C))$
138	134 137	eqtrd	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} F = (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{-} (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C))$
139	138 10	oveq12d	$⊢ φ \to (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E = ((\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k) \underset{˙}{\cdot} A)) \underset{˙}{-} (\underset{k \in (0 ..^N)}{\sum_{R}}, (D (k + 1) \underset{˙}{\cdot} C))) \underset{˙}{+} ((D (N) \underset{˙}{\cdot} A) \underset{˙}{-} (D (0) \underset{˙}{\cdot} C))$
140	129 132 139	3eqtr4d	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} (A \underset{˙}{-} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$

Metamath Proof Explorer

Theorem gsummulsubdishift1

Proof