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

Metamath Proof Explorer

Theorem gsummulsubdishift1

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 )
gsummulsubdishift.d 
|- ( ph -> D : ( 0 ... N ) --> B )
gsummulsubdishift1.e 
|- ( ph -> E = ( ( ( D ` N ) .x. A ) .- ( ( D ` 0 ) .x. C ) ) )
gsummulsubdishift1.f 
|- ( ( ph /\ k e. ( 0 ..^ N ) ) -> F = ( ( ( D ` k ) .x. A ) .- ( ( D ` ( k + 1 ) ) .x. C ) ) )
Assertion gsummulsubdishift1 
|- ( ph -> ( ( R gsum D ) .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 gsummulsubdishift.d 
 |-  ( ph -> D : ( 0 ... N ) --> B )
10 gsummulsubdishift1.e 
 |-  ( ph -> E = ( ( ( D ` N ) .x. A ) .- ( ( D ` 0 ) .x. C ) ) )
11 gsummulsubdishift1.f 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> F = ( ( ( D ` k ) .x. A ) .- ( ( D ` ( k + 1 ) ) .x. C ) ) )
12 5 ringcmnd 
 |-  ( ph -> R e. CMnd )
13 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
14 9 ffvelcdmda 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) e. B )
15 14 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... N ) ( D ` k ) e. B )
16 1 12 13 15 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) e. B )
17 1 4 3 5 16 6 7 ringsubdi 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. ( A .- C ) ) = ( ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. A ) .- ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. C ) ) )
18 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
19 8 18 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
20 fzisfzounsn 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ... N ) = ( ( 0 ..^ N ) u. { N } ) )
21 19 20 syl 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ..^ N ) u. { N } ) )
22 21 mpteq1d 
 |-  ( ph -> ( k e. ( 0 ... N ) |-> ( ( D ` k ) .x. A ) ) = ( k e. ( ( 0 ..^ N ) u. { N } ) |-> ( ( D ` k ) .x. A ) ) )
23 22 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( D ` k ) .x. A ) ) ) = ( R gsum ( k e. ( ( 0 ..^ N ) u. { N } ) |-> ( ( D ` k ) .x. A ) ) ) )
24 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
25 eqid 
 |-  ( k e. ( 0 ... N ) |-> ( D ` k ) ) = ( k e. ( 0 ... N ) |-> ( D ` k ) )
26 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
27 25 13 14 26 fsuppmptdm 
 |-  ( ph -> ( k e. ( 0 ... N ) |-> ( D ` k ) ) finSupp ( 0g ` R ) )
28 1 24 4 5 13 6 14 27 gsummulc1 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( D ` k ) .x. A ) ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. A ) )
29 fzofi 
 |-  ( 0 ..^ N ) e. Fin
30 29 a1i 
 |-  ( ph -> ( 0 ..^ N ) e. Fin )
31 5 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> R e. Ring )
32 fzossfz 
 |-  ( 0 ..^ N ) C_ ( 0 ... N )
33 32 a1i 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ... N ) )
34 33 sselda 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> k e. ( 0 ... N ) )
35 34 14 syldan 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( D ` k ) e. B )
36 6 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> A e. B )
37 1 4 31 35 36 ringcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( D ` k ) .x. A ) e. B )
38 fzonel 
 |-  -. N e. ( 0 ..^ N )
39 38 a1i 
 |-  ( ph -> -. N e. ( 0 ..^ N ) )
40 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
41 8 40 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
42 9 41 ffvelcdmd 
 |-  ( ph -> ( D ` N ) e. B )
43 1 4 5 42 6 ringcld 
 |-  ( ph -> ( ( D ` N ) .x. A ) e. B )
44 fveq2 
 |-  ( k = N -> ( D ` k ) = ( D ` N ) )
45 44 oveq1d 
 |-  ( k = N -> ( ( D ` k ) .x. A ) = ( ( D ` N ) .x. A ) )
46 1 2 12 30 37 8 39 43 45 gsumunsn 
 |-  ( ph -> ( R gsum ( k e. ( ( 0 ..^ N ) u. { N } ) |-> ( ( D ` k ) .x. A ) ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .+ ( ( D ` N ) .x. A ) ) )
47 23 28 46 3eqtr3d 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. A ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .+ ( ( D ` N ) .x. A ) ) )
48 1 24 4 5 13 7 14 27 gsummulc1 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( D ` k ) .x. C ) ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. C ) )
49 fz0sn0fz1 
 |-  ( N e. NN0 -> ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) )
50 8 49 syl 
 |-  ( ph -> ( 0 ... N ) = ( { 0 } u. ( 1 ... N ) ) )
51 uncom 
 |-  ( ( 1 ... N ) u. { 0 } ) = ( { 0 } u. ( 1 ... N ) )
52 50 51 eqtr4di 
 |-  ( ph -> ( 0 ... N ) = ( ( 1 ... N ) u. { 0 } ) )
53 52 mpteq1d 
 |-  ( ph -> ( k e. ( 0 ... N ) |-> ( ( D ` k ) .x. C ) ) = ( k e. ( ( 1 ... N ) u. { 0 } ) |-> ( ( D ` k ) .x. C ) ) )
54 53 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( D ` k ) .x. C ) ) ) = ( R gsum ( k e. ( ( 1 ... N ) u. { 0 } ) |-> ( ( D ` k ) .x. C ) ) ) )
55 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
56 5 adantr 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> R e. Ring )
57 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
58 57 a1i 
 |-  ( ph -> ( 1 ... N ) C_ ( 0 ... N ) )
59 58 sselda 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> k e. ( 0 ... N ) )
60 59 14 syldan 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( D ` k ) e. B )
61 7 adantr 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> C e. B )
62 1 4 56 60 61 ringcld 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( ( D ` k ) .x. C ) e. B )
63 c0ex 
 |-  0 e. _V
64 63 a1i 
 |-  ( ph -> 0 e. _V )
65 0nnn 
 |-  -. 0 e. NN
66 elfznn 
 |-  ( 0 e. ( 1 ... N ) -> 0 e. NN )
67 65 66 mto 
 |-  -. 0 e. ( 1 ... N )
68 67 a1i 
 |-  ( ph -> -. 0 e. ( 1 ... N ) )
69 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
70 8 69 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
71 9 70 ffvelcdmd 
 |-  ( ph -> ( D ` 0 ) e. B )
72 1 4 5 71 7 ringcld 
 |-  ( ph -> ( ( D ` 0 ) .x. C ) e. B )
73 fveq2 
 |-  ( k = 0 -> ( D ` k ) = ( D ` 0 ) )
74 73 oveq1d 
 |-  ( k = 0 -> ( ( D ` k ) .x. C ) = ( ( D ` 0 ) .x. C ) )
75 1 2 12 55 62 64 68 72 74 gsumunsn 
 |-  ( ph -> ( R gsum ( k e. ( ( 1 ... N ) u. { 0 } ) |-> ( ( D ` k ) .x. C ) ) ) = ( ( R gsum ( k e. ( 1 ... N ) |-> ( ( D ` k ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) )
76 nfcv 
 |-  F/_ k ( ( D ` ( l + 1 ) ) .x. C )
77 fveq2 
 |-  ( k = ( l + 1 ) -> ( D ` k ) = ( D ` ( l + 1 ) ) )
78 77 oveq1d 
 |-  ( k = ( l + 1 ) -> ( ( D ` k ) .x. C ) = ( ( D ` ( l + 1 ) ) .x. C ) )
79 ssidd 
 |-  ( ph -> B C_ B )
80 8 nn0zd 
 |-  ( ph -> N e. ZZ )
81 fzoval 
 |-  ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
82 80 81 syl 
 |-  ( ph -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
83 82 eleq2d 
 |-  ( ph -> ( l e. ( 0 ..^ N ) <-> l e. ( 0 ... ( N - 1 ) ) ) )
84 83 biimpar 
 |-  ( ( ph /\ l e. ( 0 ... ( N - 1 ) ) ) -> l e. ( 0 ..^ N ) )
85 fz0add1fz1 
 |-  ( ( N e. NN0 /\ l e. ( 0 ..^ N ) ) -> ( l + 1 ) e. ( 1 ... N ) )
86 8 84 85 syl2an2r 
 |-  ( ( ph /\ l e. ( 0 ... ( N - 1 ) ) ) -> ( l + 1 ) e. ( 1 ... N ) )
87 59 elfzelzd 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> k e. ZZ )
88 80 adantr 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> N e. ZZ )
89 simpr 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> k e. ( 1 ... N ) )
90 elfzm1b 
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k e. ( 1 ... N ) <-> ( k - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
91 90 biimpa 
 |-  ( ( ( k e. ZZ /\ N e. ZZ ) /\ k e. ( 1 ... N ) ) -> ( k - 1 ) e. ( 0 ... ( N - 1 ) ) )
92 87 88 89 91 syl21anc 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> ( k - 1 ) e. ( 0 ... ( N - 1 ) ) )
93 eqcom 
 |-  ( ( l + 1 ) = k <-> k = ( l + 1 ) )
94 elfznn0 
 |-  ( l e. ( 0 ... ( N - 1 ) ) -> l e. NN0 )
95 94 nn0cnd 
 |-  ( l e. ( 0 ... ( N - 1 ) ) -> l e. CC )
96 95 adantl 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ l e. ( 0 ... ( N - 1 ) ) ) -> l e. CC )
97 1cnd 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ l e. ( 0 ... ( N - 1 ) ) ) -> 1 e. CC )
98 87 zcnd 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> k e. CC )
99 98 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ l e. ( 0 ... ( N - 1 ) ) ) -> k e. CC )
100 96 97 99 addlsub 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ l e. ( 0 ... ( N - 1 ) ) ) -> ( ( l + 1 ) = k <-> l = ( k - 1 ) ) )
101 93 100 bitr3id 
 |-  ( ( ( ph /\ k e. ( 1 ... N ) ) /\ l e. ( 0 ... ( N - 1 ) ) ) -> ( k = ( l + 1 ) <-> l = ( k - 1 ) ) )
102 92 101 reu6dv 
 |-  ( ( ph /\ k e. ( 1 ... N ) ) -> E! l e. ( 0 ... ( N - 1 ) ) k = ( l + 1 ) )
103 76 1 24 78 12 55 79 62 86 102 gsummptf1o 
 |-  ( ph -> ( R gsum ( k e. ( 1 ... N ) |-> ( ( D ` k ) .x. C ) ) ) = ( R gsum ( l e. ( 0 ... ( N - 1 ) ) |-> ( ( D ` ( l + 1 ) ) .x. C ) ) ) )
104 fvoveq1 
 |-  ( l = k -> ( D ` ( l + 1 ) ) = ( D ` ( k + 1 ) ) )
105 104 oveq1d 
 |-  ( l = k -> ( ( D ` ( l + 1 ) ) .x. C ) = ( ( D ` ( k + 1 ) ) .x. C ) )
106 105 cbvmptv 
 |-  ( l e. ( 0 ... ( N - 1 ) ) |-> ( ( D ` ( l + 1 ) ) .x. C ) ) = ( k e. ( 0 ... ( N - 1 ) ) |-> ( ( D ` ( k + 1 ) ) .x. C ) )
107 82 mpteq1d 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) = ( k e. ( 0 ... ( N - 1 ) ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) )
108 106 107 eqtr4id 
 |-  ( ph -> ( l e. ( 0 ... ( N - 1 ) ) |-> ( ( D ` ( l + 1 ) ) .x. C ) ) = ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) )
109 108 oveq2d 
 |-  ( ph -> ( R gsum ( l e. ( 0 ... ( N - 1 ) ) |-> ( ( D ` ( l + 1 ) ) .x. C ) ) ) = ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) )
110 103 109 eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( 1 ... N ) |-> ( ( D ` k ) .x. C ) ) ) = ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) )
111 110 oveq1d 
 |-  ( ph -> ( ( R gsum ( k e. ( 1 ... N ) |-> ( ( D ` k ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) )
112 54 75 111 3eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( 0 ... N ) |-> ( ( D ` k ) .x. C ) ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) )
113 48 112 eqtr3d 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. C ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) )
114 47 113 oveq12d 
 |-  ( ph -> ( ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. A ) .- ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. C ) ) = ( ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .+ ( ( D ` N ) .x. A ) ) .- ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) ) )
115 5 ringabld 
 |-  ( ph -> R e. Abel )
116 37 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ..^ N ) ( ( D ` k ) .x. A ) e. B )
117 1 12 30 116 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) e. B )
118 9 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> D : ( 0 ... N ) --> B )
119 fz0add1fz1 
 |-  ( ( N e. NN0 /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 1 ... N ) )
120 8 119 sylan 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 1 ... N ) )
121 57 120 sselid 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( k + 1 ) e. ( 0 ... N ) )
122 118 121 ffvelcdmd 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( D ` ( k + 1 ) ) e. B )
123 7 adantr 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> C e. B )
124 1 4 31 122 123 ringcld 
 |-  ( ( ph /\ k e. ( 0 ..^ N ) ) -> ( ( D ` ( k + 1 ) ) .x. C ) e. B )
125 124 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ..^ N ) ( ( D ` ( k + 1 ) ) .x. C ) e. B )
126 1 12 30 125 gsummptcl 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) e. B )
127 1 2 3 ablsub4 
 |-  ( ( R e. Abel /\ ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) e. B /\ ( ( D ` N ) .x. A ) e. B ) /\ ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) e. B /\ ( ( D ` 0 ) .x. C ) e. B ) ) -> ( ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .+ ( ( D ` N ) .x. A ) ) .- ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) ) = ( ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .- ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) .+ ( ( ( D ` N ) .x. A ) .- ( ( D ` 0 ) .x. C ) ) ) )
128 115 117 43 126 72 127 syl122anc 
 |-  ( ph -> ( ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .+ ( ( D ` N ) .x. A ) ) .- ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) .+ ( ( D ` 0 ) .x. C ) ) ) = ( ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .- ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) .+ ( ( ( D ` N ) .x. A ) .- ( ( D ` 0 ) .x. C ) ) ) )
129 17 114 128 3eqtrd 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. ( A .- C ) ) = ( ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .- ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) .+ ( ( ( D ` N ) .x. A ) .- ( ( D ` 0 ) .x. C ) ) ) )
130 9 feqmptd 
 |-  ( ph -> D = ( k e. ( 0 ... N ) |-> ( D ` k ) ) )
131 130 oveq2d 
 |-  ( ph -> ( R gsum D ) = ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) )
132 131 oveq1d 
 |-  ( ph -> ( ( R gsum D ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ... N ) |-> ( D ` k ) ) ) .x. ( A .- C ) ) )
133 11 mpteq2dva 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> F ) = ( k e. ( 0 ..^ N ) |-> ( ( ( D ` k ) .x. A ) .- ( ( D ` ( k + 1 ) ) .x. C ) ) ) )
134 133 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) = ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( ( D ` k ) .x. A ) .- ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) )
135 eqid 
 |-  ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) = ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) )
136 eqid 
 |-  ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) = ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) )
137 1 3 115 30 37 124 135 136 gsummptfidmsub 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( ( D ` k ) .x. A ) .- ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .- ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) )
138 134 137 eqtrd 
 |-  ( ph -> ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .- ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) )
139 138 10 oveq12d 
 |-  ( ph -> ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) = ( ( ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` k ) .x. A ) ) ) .- ( R gsum ( k e. ( 0 ..^ N ) |-> ( ( D ` ( k + 1 ) ) .x. C ) ) ) ) .+ ( ( ( D ` N ) .x. A ) .- ( ( D ` 0 ) .x. C ) ) ) )
140 129 132 139 3eqtr4d 
 |-  ( ph -> ( ( R gsum D ) .x. ( A .- C ) ) = ( ( R gsum ( k e. ( 0 ..^ N ) |-> F ) ) .+ E ) )