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