gsummulsubdishift2s

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}$
	gsummulsubdishifts.d	$⊢ (φ \land i \in (0 \dots N)) \to V \in B$
	gsummulsubdishift2s.1	$⊢ i = 0 \to V = G$
	gsummulsubdishift2s.2	$⊢ i = N \to V = H$
	gsummulsubdishift2s.3	$⊢ i = k \to V = P$
	gsummulsubdishift2s.4	$⊢ i = k + 1 \to V = Q$
	gsummulsubdishift2s.e	$⊢ φ \to E = (G \underset{˙}{\cdot} A) \underset{˙}{-} (H \underset{˙}{\cdot} C)$
	gsummulsubdishift2s.f	$⊢ (φ \land k \in (0 ..^N)) \to F = (Q \underset{˙}{\cdot} A) \underset{˙}{-} (P \underset{˙}{\cdot} C)$
Assertion	gsummulsubdishift2s	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, P) \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		gsummulsubdishifts.d	$⊢ (φ \land i \in (0 \dots N)) \to V \in B$
10		gsummulsubdishift2s.1	$⊢ i = 0 \to V = G$
11		gsummulsubdishift2s.2	$⊢ i = N \to V = H$
12		gsummulsubdishift2s.3	$⊢ i = k \to V = P$
13		gsummulsubdishift2s.4	$⊢ i = k + 1 \to V = Q$
14		gsummulsubdishift2s.e	$⊢ φ \to E = (G \underset{˙}{\cdot} A) \underset{˙}{-} (H \underset{˙}{\cdot} C)$
15		gsummulsubdishift2s.f	$⊢ (φ \land k \in (0 ..^N)) \to F = (Q \underset{˙}{\cdot} A) \underset{˙}{-} (P \underset{˙}{\cdot} C)$
16	12	cbvmptv	$⊢ (i \in (0 \dots N) ⟼ V) = (k \in (0 \dots N) ⟼ P)$
17	16	oveq2i	$⊢ {\sum_{R}}_{i = 0}^{N} V = {\sum_{R}}_{k = 0}^{N} P$
18	17	oveq1i	$⊢ ({\sum_{R}}_{i = 0}^{N}, V) \underset{˙}{\cdot} (A \underset{˙}{-} C) = ({\sum_{R}}_{k = 0}^{N}, P) \underset{˙}{\cdot} (A \underset{˙}{-} C)$
19	9	fmpttd	$⊢ φ \to (i \in (0 \dots N) ⟼ V) : (0 \dots N) ⟶ B$
20		eqid	$⊢ (i \in (0 \dots N) ⟼ V) = (i \in (0 \dots N) ⟼ V)$
21		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
22	8 21	syl	$⊢ φ \to 0 \in (0 \dots N)$
23		c0ex	$⊢ 0 \in V$
24	23 10	csbie	$⊢ ⦋ 0 / i ⦌ V = G$
25	9	ralrimiva	$⊢ φ \to \forall i \in (0 \dots N) V \in B$
26		rspcsbela	$⊢ (0 \in (0 \dots N) \land \forall i \in (0 \dots N) V \in B) \to ⦋ 0 / i ⦌ V \in B$
27	22 25 26	syl2anc	$⊢ φ \to ⦋ 0 / i ⦌ V \in B$
28	24 27	eqeltrrid	$⊢ φ \to G \in B$
29	20 10 22 28	fvmptd3	$⊢ φ \to (i \in (0 \dots N) ⟼ V) (0) = G$
30	29	oveq1d	$⊢ φ \to (i \in (0 \dots N) ⟼ V) (0) \underset{˙}{\cdot} A = G \underset{˙}{\cdot} A$
31		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
32	8 31	sylib	$⊢ φ \to N \in (0 \dots N)$
33	11	adantl	$⊢ (φ \land i = N) \to V = H$
34	8 33	csbied	$⊢ φ \to ⦋ N / i ⦌ V = H$
35		rspcsbela	$⊢ (N \in (0 \dots N) \land \forall i \in (0 \dots N) V \in B) \to ⦋ N / i ⦌ V \in B$
36	32 25 35	syl2anc	$⊢ φ \to ⦋ N / i ⦌ V \in B$
37	34 36	eqeltrrd	$⊢ φ \to H \in B$
38	20 11 32 37	fvmptd3	$⊢ φ \to (i \in (0 \dots N) ⟼ V) (N) = H$
39	38	oveq1d	$⊢ φ \to (i \in (0 \dots N) ⟼ V) (N) \underset{˙}{\cdot} C = H \underset{˙}{\cdot} C$
40	30 39	oveq12d	$⊢ φ \to ((i \in (0 \dots N) ⟼ V) (0) \underset{˙}{\cdot} A) \underset{˙}{-} ((i \in (0 \dots N) ⟼ V) (N) \underset{˙}{\cdot} C) = (G \underset{˙}{\cdot} A) \underset{˙}{-} (H \underset{˙}{\cdot} C)$
41	14 40	eqtr4d	$⊢ φ \to E = ((i \in (0 \dots N) ⟼ V) (0) \underset{˙}{\cdot} A) \underset{˙}{-} ((i \in (0 \dots N) ⟼ V) (N) \underset{˙}{\cdot} C)$
42		fzofzp1	$⊢ k \in (0 ..^N) \to k + 1 \in (0 \dots N)$
43	42	adantl	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \in (0 \dots N)$
44	13	adantl	$⊢ ((φ \land k \in (0 ..^N)) \land i = k + 1) \to V = Q$
45	43 44	csbied	$⊢ (φ \land k \in (0 ..^N)) \to ⦋ (k + 1) / i ⦌ V = Q$
46	25	adantr	$⊢ (φ \land k \in (0 ..^N)) \to \forall i \in (0 \dots N) V \in B$
47		rspcsbela	$⊢ (k + 1 \in (0 \dots N) \land \forall i \in (0 \dots N) V \in B) \to ⦋ (k + 1) / i ⦌ V \in B$
48	43 46 47	syl2anc	$⊢ (φ \land k \in (0 ..^N)) \to ⦋ (k + 1) / i ⦌ V \in B$
49	45 48	eqeltrrd	$⊢ (φ \land k \in (0 ..^N)) \to Q \in B$
50	20 13 43 49	fvmptd3	$⊢ (φ \land k \in (0 ..^N)) \to (i \in (0 \dots N) ⟼ V) (k + 1) = Q$
51	50	oveq1d	$⊢ (φ \land k \in (0 ..^N)) \to (i \in (0 \dots N) ⟼ V) (k + 1) \underset{˙}{\cdot} A = Q \underset{˙}{\cdot} A$
52		fzossfz	$⊢ (0 ..^N) \subseteq (0 \dots N)$
53		simpr	$⊢ (φ \land k \in (0 ..^N)) \to k \in (0 ..^N)$
54	52 53	sselid	$⊢ (φ \land k \in (0 ..^N)) \to k \in (0 \dots N)$
55	12	adantl	$⊢ ((φ \land k \in (0 ..^N)) \land i = k) \to V = P$
56	53 55	csbied	$⊢ (φ \land k \in (0 ..^N)) \to ⦋ k / i ⦌ V = P$
57		rspcsbela	$⊢ (k \in (0 \dots N) \land \forall i \in (0 \dots N) V \in B) \to ⦋ k / i ⦌ V \in B$
58	54 46 57	syl2anc	$⊢ (φ \land k \in (0 ..^N)) \to ⦋ k / i ⦌ V \in B$
59	56 58	eqeltrrd	$⊢ (φ \land k \in (0 ..^N)) \to P \in B$
60	20 12 54 59	fvmptd3	$⊢ (φ \land k \in (0 ..^N)) \to (i \in (0 \dots N) ⟼ V) (k) = P$
61	60	oveq1d	$⊢ (φ \land k \in (0 ..^N)) \to (i \in (0 \dots N) ⟼ V) (k) \underset{˙}{\cdot} C = P \underset{˙}{\cdot} C$
62	51 61	oveq12d	$⊢ (φ \land k \in (0 ..^N)) \to ((i \in (0 \dots N) ⟼ V) (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} ((i \in (0 \dots N) ⟼ V) (k) \underset{˙}{\cdot} C) = (Q \underset{˙}{\cdot} A) \underset{˙}{-} (P \underset{˙}{\cdot} C)$
63	15 62	eqtr4d	$⊢ (φ \land k \in (0 ..^N)) \to F = ((i \in (0 \dots N) ⟼ V) (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} ((i \in (0 \dots N) ⟼ V) (k) \underset{˙}{\cdot} C)$
64	1 2 3 4 5 6 7 8 19 41 63	gsummulsubdishift2	$⊢ φ \to ({\sum_{R}}_{i = 0}^{N}, V) \underset{˙}{\cdot} (A \underset{˙}{-} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$
65	18 64	eqtr3id	$⊢ φ \to ({\sum_{R}}_{k = 0}^{N}, P) \underset{˙}{\cdot} (A \underset{˙}{-} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$

Metamath Proof Explorer

Theorem gsummulsubdishift2s

Proof