This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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