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 
|- B = ( Base ` R )
gsummulsubdishift.p 
|- .+ = ( +g ` R )
gsummulsubdishift.m 
|- .- = ( -g ` R )
gsummulsubdishift.t 
|- .x. = ( .r ` R )
gsummulsubdishift.r 
|- ( ph -> R e. Ring )
gsummulsubdishift.a 
|- ( ph -> A e. B )
gsummulsubdishift.c 
|- ( ph -> C e. B )
gsummulsubdishift.n 
|- ( ph -> N e. NN0 )
gsummulsubdishifts.d 
|- ( ( ph /\ i e. ( 0 ... N ) ) -> V e. B )
gsummulsubdishift2s.1 
|- ( i = 0 -> V = G )
gsummulsubdishift2s.2 
|- ( i = N -> V = H )
gsummulsubdishift2s.3 
|- ( i = k -> V = P )
gsummulsubdishift2s.4 
|- ( i = ( k + 1 ) -> V = Q )
gsummulsubdishift2s.e 
|- ( ph -> E = ( ( G .x. A ) .- ( H .x. C ) ) )
gsummulsubdishift2s.f 
|- ( ( ph /\ k e. ( 0 ..^ N ) ) -> F = ( ( Q .x. A ) .- ( P .x. C ) ) )
Assertion gsummulsubdishift2s 
|- ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> P ) ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )

Proof

Step Hyp Ref Expression
1 gsummulsubdishift.b 
 |-  B = ( Base ` R )
2 gsummulsubdishift.p 
 |-  .+ = ( +g ` R )
3 gsummulsubdishift.m 
 |-  .- = ( -g ` R )
4 gsummulsubdishift.t 
 |-  .x. = ( .r ` R )
5 gsummulsubdishift.r 
 |-  ( ph -> R e. Ring )
6 gsummulsubdishift.a 
 |-  ( ph -> A e. B )
7 gsummulsubdishift.c 
 |-  ( ph -> C e. B )
8 gsummulsubdishift.n 
 |-  ( ph -> N e. NN0 )
9 gsummulsubdishifts.d 
 |-  ( ( ph /\ i e. ( 0 ... N ) ) -> V e. B )
10 gsummulsubdishift2s.1 
 |-  ( i = 0 -> V = G )
11 gsummulsubdishift2s.2 
 |-  ( i = N -> V = H )
12 gsummulsubdishift2s.3 
 |-  ( i = k -> V = P )
13 gsummulsubdishift2s.4 
 |-  ( i = ( k + 1 ) -> V = Q )
14 gsummulsubdishift2s.e 
 |-  ( ph -> E = ( ( G .x. A ) .- ( H .x. C ) ) )
15 gsummulsubdishift2s.f 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> F = ( ( Q .x. A ) .- ( P .x. C ) ) )
16 12 cbvmptv 
 |-  ( i e. ( 0 ... N ) |-> V ) = ( k e. ( 0 ... N ) |-> P )
17 16 oveq2i 
 |-  ( R gsum ( i e. ( 0 ... N ) |-> V ) ) = ( R gsum ( k e. ( 0 ... N ) |-> P ) )
18 17 oveq1i 
 |-  ( ( R gsum ( i e. ( 0 ... N ) |-> V ) ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> P ) ) .x. ( A .- C ) )
19 9 fmpttd 
 |-  ( ph -> ( i e. ( 0 ... N ) |-> V ) : ( 0 ... N ) --> B )
20 eqid 
 |-  ( i e. ( 0 ... N ) |-> V ) = ( i e. ( 0 ... N ) |-> V )
21 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
22 8 21 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
23 c0ex 
 |-  0 e. _V
24 23 10 csbie 
 |-  [_ 0 / i ]_ V = G
25 9 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ... N ) V e. B )
26 rspcsbela 
 |-  ( ( 0 e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) V e. B ) -> [_ 0 / i ]_ V e. B )
27 22 25 26 syl2anc 
 |-  ( ph -> [_ 0 / i ]_ V e. B )
28 24 27 eqeltrrid 
 |-  ( ph -> G e. B )
29 20 10 22 28 fvmptd3 
 |-  ( ph -> ( ( i e. ( 0 ... N ) |-> V ) ` 0 ) = G )
30 29 oveq1d 
 |-  ( ph -> ( ( ( i e. ( 0 ... N ) |-> V ) ` 0 ) .x. A ) = ( G .x. A ) )
31 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
32 8 31 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
33 11 adantl 
 |-  ( ( ph /\ i = N ) -> V = H )
34 8 33 csbied 
 |-  ( ph -> [_ N / i ]_ V = H )
35 rspcsbela 
 |-  ( ( N e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) V e. B ) -> [_ N / i ]_ V e. B )
36 32 25 35 syl2anc 
 |-  ( ph -> [_ N / i ]_ V e. B )
37 34 36 eqeltrrd 
 |-  ( ph -> H e. B )
38 20 11 32 37 fvmptd3 
 |-  ( ph -> ( ( i e. ( 0 ... N ) |-> V ) ` N ) = H )
39 38 oveq1d 
 |-  ( ph -> ( ( ( i e. ( 0 ... N ) |-> V ) ` N ) .x. C ) = ( H .x. C ) )
40 30 39 oveq12d 
 |-  ( ph -> ( ( ( ( i e. ( 0 ... N ) |-> V ) ` 0 ) .x. A ) .- ( ( ( i e. ( 0 ... N ) |-> V ) ` N ) .x. C ) ) = ( ( G .x. A ) .- ( H .x. C ) ) )
41 14 40 eqtr4d 
 |-  ( ph -> E = ( ( ( ( i e. ( 0 ... N ) |-> V ) ` 0 ) .x. A ) .- ( ( ( i e. ( 0 ... N ) |-> V ) ` N ) .x. C ) ) )
42 fzofzp1 
 |-  ( k e. ( 0 ..^ N ) -> ( k + 1 ) e. ( 0 ... N ) )
43 42 adantl 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 0 ... N ) )
44 13 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ i = ( k + 1 ) ) -> V = Q )
45 43 44 csbied 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> [_ ( k + 1 ) / i ]_ V = Q )
46 25 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> A. i e. ( 0 ... N ) V e. B )
47 rspcsbela 
 |-  ( ( ( k + 1 ) e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) V e. B ) -> [_ ( k + 1 ) / i ]_ V e. B )
48 43 46 47 syl2anc 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> [_ ( k + 1 ) / i ]_ V e. B )
49 45 48 eqeltrrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> Q e. B )
50 20 13 43 49 fvmptd3 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( i e. ( 0 ... N ) |-> V ) ` ( k + 1 ) ) = Q )
51 50 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( ( i e. ( 0 ... N ) |-> V ) ` ( k + 1 ) ) .x. A ) = ( Q .x. A ) )
52 fzossfz 
 |-  ( 0 ..^ N ) C_ ( 0 ... N )
53 simpr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( 0 ..^ N ) )
54 52 53 sselid 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( 0 ... N ) )
55 12 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ..^ N ) ) /\ i = k ) -> V = P )
56 53 55 csbied 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> [_ k / i ]_ V = P )
57 rspcsbela 
 |-  ( ( k e. ( 0 ... N ) /\ A. i e. ( 0 ... N ) V e. B ) -> [_ k / i ]_ V e. B )
58 54 46 57 syl2anc 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> [_ k / i ]_ V e. B )
59 56 58 eqeltrrd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> P e. B )
60 20 12 54 59 fvmptd3 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( i e. ( 0 ... N ) |-> V ) ` k ) = P )
61 60 oveq1d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( ( i e. ( 0 ... N ) |-> V ) ` k ) .x. C ) = ( P .x. C ) )
62 51 61 oveq12d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( ( ( i e. ( 0 ... N ) |-> V ) ` ( k + 1 ) ) .x. A ) .- ( ( ( i e. ( 0 ... N ) |-> V ) ` k ) .x. C ) ) = ( ( Q .x. A ) .- ( P .x. C ) ) )
63 15 62 eqtr4d 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> F = ( ( ( ( i e. ( 0 ... N ) |-> V ) ` ( k + 1 ) ) .x. A ) .- ( ( ( i e. ( 0 ... N ) |-> V ) ` k ) .x. C ) ) )
64 1 2 3 4 5 6 7 8 19 41 63 gsummulsubdishift2 
 |-  ( ph -> ( ( R gsum ( i e. ( 0 ... N ) |-> V ) ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )
65 18 64 eqtr3id 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> P ) ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )