Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
gsummulsubdishift.p ⊢ + = ( +g ‘ 𝑅 )
gsummulsubdishift.m ⊢ − = ( -g ‘ 𝑅 )
gsummulsubdishift.t ⊢ · = ( .r ‘ 𝑅 )
gsummulsubdishift.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
gsummulsubdishift.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
gsummulsubdishift.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
gsummulsubdishift.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
gsummulsubdishifts.d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑉 ∈ 𝐵 )
gsummulsubdishift2s.1 ⊢ ( 𝑖 = 0 → 𝑉 = 𝐺 )
gsummulsubdishift2s.2 ⊢ ( 𝑖 = 𝑁 → 𝑉 = 𝐻 )
gsummulsubdishift2s.3 ⊢ ( 𝑖 = 𝑘 → 𝑉 = 𝑃 )
gsummulsubdishift2s.4 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → 𝑉 = 𝑄 )
gsummulsubdishift2s.e ⊢ ( 𝜑 → 𝐸 = ( ( 𝐺 · 𝐴 ) − ( 𝐻 · 𝐶 ) ) )
gsummulsubdishift2s.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 = ( ( 𝑄 · 𝐴 ) − ( 𝑃 · 𝐶 ) ) )
Assertion gsummulsubdishift2s ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑃 ) ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )

Proof

Step Hyp Ref Expression
1 gsummulsubdishift.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 gsummulsubdishift.p ⊢ + = ( +g ‘ 𝑅 )
3 gsummulsubdishift.m ⊢ − = ( -g ‘ 𝑅 )
4 gsummulsubdishift.t ⊢ · = ( .r ‘ 𝑅 )
5 gsummulsubdishift.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 gsummulsubdishift.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 gsummulsubdishift.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
8 gsummulsubdishift.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 gsummulsubdishifts.d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑉 ∈ 𝐵 )
10 gsummulsubdishift2s.1 ⊢ ( 𝑖 = 0 → 𝑉 = 𝐺 )
11 gsummulsubdishift2s.2 ⊢ ( 𝑖 = 𝑁 → 𝑉 = 𝐻 )
12 gsummulsubdishift2s.3 ⊢ ( 𝑖 = 𝑘 → 𝑉 = 𝑃 )
13 gsummulsubdishift2s.4 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → 𝑉 = 𝑄 )
14 gsummulsubdishift2s.e ⊢ ( 𝜑 → 𝐸 = ( ( 𝐺 · 𝐴 ) − ( 𝐻 · 𝐶 ) ) )
15 gsummulsubdishift2s.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 = ( ( 𝑄 · 𝐴 ) − ( 𝑃 · 𝐶 ) ) )
16 12 cbvmptv ⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑃 )
17 16 oveq2i ⊢ ( 𝑅 Σg ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑃 ) )
18 17 oveq1i ⊢ ( ( 𝑅 Σg ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑃 ) ) · ( 𝐴 − 𝐶 ) )
19 9 fmpttd ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) : ( 0 ... 𝑁 ) ⟶ 𝐵 )
20 eqid ⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) = ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 )
21 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
22 8 21 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
23 c0ex ⊢ 0 ∈ V
24 23 10 csbie ⊢ ⦋ 0 / 𝑖 ⦌ 𝑉 = 𝐺
25 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑉 ∈ 𝐵 )
26 rspcsbela ⊢ ( ( 0 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑉 ∈ 𝐵 ) → ⦋ 0 / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
27 22 25 26 syl2anc ⊢ ( 𝜑 → ⦋ 0 / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
28 24 27 eqeltrrid ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
29 20 10 22 28 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 0 ) = 𝐺 )
30 29 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 0 ) · 𝐴 ) = ( 𝐺 · 𝐴 ) )
31 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
32 8 31 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
33 11 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 𝑁 ) → 𝑉 = 𝐻 )
34 8 33 csbied ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑖 ⦌ 𝑉 = 𝐻 )
35 rspcsbela ⊢ ( ( 𝑁 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑉 ∈ 𝐵 ) → ⦋ 𝑁 / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
36 32 25 35 syl2anc ⊢ ( 𝜑 → ⦋ 𝑁 / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
37 34 36 eqeltrrd ⊢ ( 𝜑 → 𝐻 ∈ 𝐵 )
38 20 11 32 37 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑁 ) = 𝐻 )
39 38 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑁 ) · 𝐶 ) = ( 𝐻 · 𝐶 ) )
40 30 39 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 0 ) · 𝐴 ) − ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑁 ) · 𝐶 ) ) = ( ( 𝐺 · 𝐴 ) − ( 𝐻 · 𝐶 ) ) )
41 14 40 eqtr4d ⊢ ( 𝜑 → 𝐸 = ( ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 0 ) · 𝐴 ) − ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑁 ) · 𝐶 ) ) )
42 fzofzp1 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
44 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 = ( 𝑘 + 1 ) ) → 𝑉 = 𝑄 )
45 43 44 csbied ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ 𝑉 = 𝑄 )
46 25 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑉 ∈ 𝐵 )
47 rspcsbela ⊢ ( ( ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑉 ∈ 𝐵 ) → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
48 43 46 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
49 45 48 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑄 ∈ 𝐵 )
50 20 13 43 49 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ ( 𝑘 + 1 ) ) = 𝑄 )
51 50 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ ( 𝑘 + 1 ) ) · 𝐴 ) = ( 𝑄 · 𝐴 ) )
52 fzossfz ⊢ ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 )
53 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ..^ 𝑁 ) )
54 52 53 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
55 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 = 𝑘 ) → 𝑉 = 𝑃 )
56 53 55 csbied ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ⦋ 𝑘 / 𝑖 ⦌ 𝑉 = 𝑃 )
57 rspcsbela ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑉 ∈ 𝐵 ) → ⦋ 𝑘 / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
58 54 46 57 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ⦋ 𝑘 / 𝑖 ⦌ 𝑉 ∈ 𝐵 )
59 56 58 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑃 ∈ 𝐵 )
60 20 12 54 59 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑘 ) = 𝑃 )
61 60 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑘 ) · 𝐶 ) = ( 𝑃 · 𝐶 ) )
62 51 61 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑘 ) · 𝐶 ) ) = ( ( 𝑄 · 𝐴 ) − ( 𝑃 · 𝐶 ) ) )
63 15 62 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 = ( ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ‘ 𝑘 ) · 𝐶 ) ) )
64 1 2 3 4 5 6 7 8 19 41 63 gsummulsubdishift2 ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑖 ∈ ( 0 ... 𝑁 ) ↦ 𝑉 ) ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )
65 18 64 eqtr3id ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑃 ) ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )