gsummulsubdishift1s

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

Proof