Metamath Proof Explorer


Theorem chfacfscmulgsum

Description: Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019)

Ref Expression
Hypotheses chfacfisf.a A=NMatR
chfacfisf.b B=BaseA
chfacfisf.p P=Poly1R
chfacfisf.y Y=NMatP
chfacfisf.r ×˙=Y
chfacfisf.s -˙=-Y
chfacfisf.0 0˙=0Y
chfacfisf.t T=NmatToPolyMatR
chfacfisf.g G=n0ifn=00˙-˙TM×˙Tb0ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn
chfacfscmulcl.x X=var1R
chfacfscmulcl.m ·˙=Y
chfacfscmulcl.e ×˙=mulGrpP
chfacfscmulgsum.p +˙=+Y
Assertion chfacfscmulgsum NFinRCRingMBsbB0sYi0i×˙X·˙Gi=Yi=1si×˙X·˙Tbi1-˙TM×˙Tbi+˙s+1×˙X·˙Tbs-˙TM×˙Tb0

Proof

Step Hyp Ref Expression
1 chfacfisf.a A=NMatR
2 chfacfisf.b B=BaseA
3 chfacfisf.p P=Poly1R
4 chfacfisf.y Y=NMatP
5 chfacfisf.r ×˙=Y
6 chfacfisf.s -˙=-Y
7 chfacfisf.0 0˙=0Y
8 chfacfisf.t T=NmatToPolyMatR
9 chfacfisf.g G=n0ifn=00˙-˙TM×˙Tb0ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn
10 chfacfscmulcl.x X=var1R
11 chfacfscmulcl.m ·˙=Y
12 chfacfscmulcl.e ×˙=mulGrpP
13 chfacfscmulgsum.p +˙=+Y
14 eqid BaseY=BaseY
15 crngring RCRingRRing
16 15 anim2i NFinRCRingNFinRRing
17 16 3adant3 NFinRCRingMBNFinRRing
18 3 4 pmatring NFinRRingYRing
19 17 18 syl NFinRCRingMBYRing
20 ringcmn YRingYCMnd
21 19 20 syl NFinRCRingMBYCMnd
22 21 adantr NFinRCRingMBsbB0sYCMnd
23 nn0ex 0V
24 23 a1i NFinRCRingMBsbB0s0V
25 simpll NFinRCRingMBsbB0si0NFinRCRingMB
26 simplr NFinRCRingMBsbB0si0sbB0s
27 simpr NFinRCRingMBsbB0si0i0
28 25 26 27 3jca NFinRCRingMBsbB0si0NFinRCRingMBsbB0si0
29 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl NFinRCRingMBsbB0si0i×˙X·˙GiBaseY
30 28 29 syl NFinRCRingMBsbB0si0i×˙X·˙GiBaseY
31 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulfsupp NFinRCRingMBsbB0sfinSupp0˙i0i×˙X·˙Gi
32 nn0disj 0s+1s+1+1=
33 32 a1i NFinRCRingMBsbB0s0s+1s+1+1=
34 nnnn0 ss0
35 peano2nn0 s0s+10
36 34 35 syl ss+10
37 nn0split s+100=0s+1s+1+1
38 36 37 syl s0=0s+1s+1+1
39 38 ad2antrl NFinRCRingMBsbB0s0=0s+1s+1+1
40 14 7 13 22 24 30 31 33 39 gsumsplit2 NFinRCRingMBsbB0sYi0i×˙X·˙Gi=Yi=0s+1i×˙X·˙Gi+˙Yis+1+1i×˙X·˙Gi
41 simpll NFinRCRingMBsbB0sis+1+1NFinRCRingMB
42 simplr NFinRCRingMBsbB0sis+1+1sbB0s
43 nncn ss
44 add1p1 ss+1+1=s+2
45 43 44 syl ss+1+1=s+2
46 45 ad2antrl NFinRCRingMBsbB0ss+1+1=s+2
47 46 fveq2d NFinRCRingMBsbB0ss+1+1=s+2
48 47 eleq2d NFinRCRingMBsbB0sis+1+1is+2
49 48 biimpa NFinRCRingMBsbB0sis+1+1is+2
50 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmul0 NFinRCRingMBsbB0sis+2i×˙X·˙Gi=0˙
51 41 42 49 50 syl3anc NFinRCRingMBsbB0sis+1+1i×˙X·˙Gi=0˙
52 51 mpteq2dva NFinRCRingMBsbB0sis+1+1i×˙X·˙Gi=is+1+10˙
53 52 oveq2d NFinRCRingMBsbB0sYis+1+1i×˙X·˙Gi=Yis+1+10˙
54 15 18 sylan2 NFinRCRingYRing
55 ringmnd YRingYMnd
56 54 55 syl NFinRCRingYMnd
57 56 3adant3 NFinRCRingMBYMnd
58 fvex s+1+1V
59 57 58 jctir NFinRCRingMBYMnds+1+1V
60 59 adantr NFinRCRingMBsbB0sYMnds+1+1V
61 7 gsumz YMnds+1+1VYis+1+10˙=0˙
62 60 61 syl NFinRCRingMBsbB0sYis+1+10˙=0˙
63 53 62 eqtrd NFinRCRingMBsbB0sYis+1+1i×˙X·˙Gi=0˙
64 63 oveq2d NFinRCRingMBsbB0sYi=0s+1i×˙X·˙Gi+˙Yis+1+1i×˙X·˙Gi=Yi=0s+1i×˙X·˙Gi+˙0˙
65 fzfid NFinRCRingMBsbB0s0s+1Fin
66 elfznn0 i0s+1i0
67 66 28 sylan2 NFinRCRingMBsbB0si0s+1NFinRCRingMBsbB0si0
68 67 29 syl NFinRCRingMBsbB0si0s+1i×˙X·˙GiBaseY
69 68 ralrimiva NFinRCRingMBsbB0si0s+1i×˙X·˙GiBaseY
70 14 22 65 69 gsummptcl NFinRCRingMBsbB0sYi=0s+1i×˙X·˙GiBaseY
71 14 13 7 mndrid YMndYi=0s+1i×˙X·˙GiBaseYYi=0s+1i×˙X·˙Gi+˙0˙=Yi=0s+1i×˙X·˙Gi
72 57 70 71 syl2an2r NFinRCRingMBsbB0sYi=0s+1i×˙X·˙Gi+˙0˙=Yi=0s+1i×˙X·˙Gi
73 64 72 eqtrd NFinRCRingMBsbB0sYi=0s+1i×˙X·˙Gi+˙Yis+1+1i×˙X·˙Gi=Yi=0s+1i×˙X·˙Gi
74 34 ad2antrl NFinRCRingMBsbB0ss0
75 14 13 22 74 68 gsummptfzsplit NFinRCRingMBsbB0sYi=0s+1i×˙X·˙Gi=Yi=0si×˙X·˙Gi+˙Yis+1i×˙X·˙Gi
76 elfznn0 i0si0
77 76 30 sylan2 NFinRCRingMBsbB0si0si×˙X·˙GiBaseY
78 14 13 22 74 77 gsummptfzsplitl NFinRCRingMBsbB0sYi=0si×˙X·˙Gi=Yi=1si×˙X·˙Gi+˙Yi0i×˙X·˙Gi
79 57 adantr NFinRCRingMBsbB0sYMnd
80 0nn0 00
81 80 a1i NFinRCRingMBsbB0s00
82 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl NFinRCRingMBsbB0s000×˙X·˙G0BaseY
83 81 82 mpd3an3 NFinRCRingMBsbB0s0×˙X·˙G0BaseY
84 oveq1 i=0i×˙X=0×˙X
85 fveq2 i=0Gi=G0
86 84 85 oveq12d i=0i×˙X·˙Gi=0×˙X·˙G0
87 14 86 gsumsn YMnd000×˙X·˙G0BaseYYi0i×˙X·˙Gi=0×˙X·˙G0
88 79 81 83 87 syl3anc NFinRCRingMBsbB0sYi0i×˙X·˙Gi=0×˙X·˙G0
89 88 oveq2d NFinRCRingMBsbB0sYi=1si×˙X·˙Gi+˙Yi0i×˙X·˙Gi=Yi=1si×˙X·˙Gi+˙0×˙X·˙G0
90 78 89 eqtrd NFinRCRingMBsbB0sYi=0si×˙X·˙Gi=Yi=1si×˙X·˙Gi+˙0×˙X·˙G0
91 ovexd NFinRCRingMBsbB0ss+1V
92 1nn0 10
93 92 a1i NFinRCRingMBsbB0s10
94 74 93 nn0addcld NFinRCRingMBsbB0ss+10
95 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl NFinRCRingMBsbB0ss+10s+1×˙X·˙Gs+1BaseY
96 94 95 mpd3an3 NFinRCRingMBsbB0ss+1×˙X·˙Gs+1BaseY
97 oveq1 i=s+1i×˙X=s+1×˙X
98 fveq2 i=s+1Gi=Gs+1
99 97 98 oveq12d i=s+1i×˙X·˙Gi=s+1×˙X·˙Gs+1
100 14 99 gsumsn YMnds+1Vs+1×˙X·˙Gs+1BaseYYis+1i×˙X·˙Gi=s+1×˙X·˙Gs+1
101 79 91 96 100 syl3anc NFinRCRingMBsbB0sYis+1i×˙X·˙Gi=s+1×˙X·˙Gs+1
102 90 101 oveq12d NFinRCRingMBsbB0sYi=0si×˙X·˙Gi+˙Yis+1i×˙X·˙Gi=Yi=1si×˙X·˙Gi+˙0×˙X·˙G0+˙s+1×˙X·˙Gs+1
103 fzfid NFinRCRingMBsbB0s1sFin
104 simpll NFinRCRingMBsbB0si1sNFinRCRingMB
105 simplr NFinRCRingMBsbB0si1ssbB0s
106 elfznn i1si
107 106 nnnn0d i1si0
108 107 adantl NFinRCRingMBsbB0si1si0
109 104 105 108 29 syl3anc NFinRCRingMBsbB0si1si×˙X·˙GiBaseY
110 109 ralrimiva NFinRCRingMBsbB0si1si×˙X·˙GiBaseY
111 14 22 103 110 gsummptcl NFinRCRingMBsbB0sYi=1si×˙X·˙GiBaseY
112 14 13 mndass YMndYi=1si×˙X·˙GiBaseY0×˙X·˙G0BaseYs+1×˙X·˙Gs+1BaseYYi=1si×˙X·˙Gi+˙0×˙X·˙G0+˙s+1×˙X·˙Gs+1=Yi=1si×˙X·˙Gi+˙0×˙X·˙G0+˙s+1×˙X·˙Gs+1
113 79 111 83 96 112 syl13anc NFinRCRingMBsbB0sYi=1si×˙X·˙Gi+˙0×˙X·˙G0+˙s+1×˙X·˙Gs+1=Yi=1si×˙X·˙Gi+˙0×˙X·˙G0+˙s+1×˙X·˙Gs+1
114 106 nnne0d i1si0
115 114 ad2antlr NFinRCRingMBsbB0si1sn=ii0
116 neeq1 n=in0i0
117 116 adantl NFinRCRingMBsbB0si1sn=in0i0
118 115 117 mpbird NFinRCRingMBsbB0si1sn=in0
119 eqneqall n=0n00˙=Tbi1
120 118 119 mpan9 NFinRCRingMBsbB0si1sn=in=00˙=Tbi1
121 simplr NFinRCRingMBsbB0si1sn=in=0n=i
122 eqeq1 0=n0=in=i
123 122 eqcoms n=00=in=i
124 123 adantl NFinRCRingMBsbB0si1sn=in=00=in=i
125 121 124 mpbird NFinRCRingMBsbB0si1sn=in=00=i
126 125 fveq2d NFinRCRingMBsbB0si1sn=in=0b0=bi
127 126 fveq2d NFinRCRingMBsbB0si1sn=in=0Tb0=Tbi
128 127 oveq2d NFinRCRingMBsbB0si1sn=in=0TM×˙Tb0=TM×˙Tbi
129 120 128 oveq12d NFinRCRingMBsbB0si1sn=in=00˙-˙TM×˙Tb0=Tbi1-˙TM×˙Tbi
130 elfz2 i1s1si1iis
131 zleltp1 isisi<s+1
132 131 ancoms siisi<s+1
133 132 3adant1 1siisi<s+1
134 133 biimpcd is1sii<s+1
135 134 adantl 1iis1sii<s+1
136 135 impcom 1si1iisi<s+1
137 136 orcd 1si1iisi<s+1s+1<i
138 zre ss
139 1red s1
140 138 139 readdcld ss+1
141 zre ii
142 140 141 anim12ci siis+1
143 142 3adant1 1siis+1
144 lttri2 is+1is+1i<s+1s+1<i
145 143 144 syl 1siis+1i<s+1s+1<i
146 145 adantr 1si1iisis+1i<s+1s+1<i
147 137 146 mpbird 1si1iisis+1
148 130 147 sylbi i1sis+1
149 148 ad2antlr NFinRCRingMBsbB0si1sn=iis+1
150 neeq1 n=ins+1is+1
151 150 adantl NFinRCRingMBsbB0si1sn=ins+1is+1
152 149 151 mpbird NFinRCRingMBsbB0si1sn=ins+1
153 152 adantr NFinRCRingMBsbB0si1sn=i¬n=0ns+1
154 153 neneqd NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1
155 154 pm2.21d NFinRCRingMBsbB0si1sn=i¬n=0n=s+1Tbs=Tbi1-˙TM×˙Tbi
156 155 imp NFinRCRingMBsbB0si1sn=i¬n=0n=s+1Tbs=Tbi1-˙TM×˙Tbi
157 106 nnred i1si
158 eleq1w n=ini
159 157 158 syl5ibrcom i1sn=in
160 159 adantl NFinRCRingMBsbB0si1sn=in
161 160 imp NFinRCRingMBsbB0si1sn=in
162 74 nn0red NFinRCRingMBsbB0ss
163 162 ad2antrr NFinRCRingMBsbB0si1sn=is
164 1red NFinRCRingMBsbB0si1sn=i1
165 163 164 readdcld NFinRCRingMBsbB0si1sn=is+1
166 130 136 sylbi i1si<s+1
167 166 ad2antlr NFinRCRingMBsbB0si1sn=ii<s+1
168 breq1 n=in<s+1i<s+1
169 168 adantl NFinRCRingMBsbB0si1sn=in<s+1i<s+1
170 167 169 mpbird NFinRCRingMBsbB0si1sn=in<s+1
171 161 165 170 ltnsymd NFinRCRingMBsbB0si1sn=i¬s+1<n
172 171 pm2.21d NFinRCRingMBsbB0si1sn=is+1<n0˙=Tbi1-˙TM×˙Tbi
173 172 ad2antrr NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1s+1<n0˙=Tbi1-˙TM×˙Tbi
174 173 imp NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1s+1<n0˙=Tbi1-˙TM×˙Tbi
175 simp-4r NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1¬s+1<nn=i
176 175 fvoveq1d NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1¬s+1<nbn1=bi1
177 176 fveq2d NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1¬s+1<nTbn1=Tbi1
178 175 fveq2d NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1¬s+1<nbn=bi
179 178 fveq2d NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1¬s+1<nTbn=Tbi
180 179 oveq2d NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1¬s+1<nTM×˙Tbn=TM×˙Tbi
181 177 180 oveq12d NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1¬s+1<nTbn1-˙TM×˙Tbn=Tbi1-˙TM×˙Tbi
182 174 181 ifeqda NFinRCRingMBsbB0si1sn=i¬n=0¬n=s+1ifs+1<n0˙Tbn1-˙TM×˙Tbn=Tbi1-˙TM×˙Tbi
183 156 182 ifeqda NFinRCRingMBsbB0si1sn=i¬n=0ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn=Tbi1-˙TM×˙Tbi
184 129 183 ifeqda NFinRCRingMBsbB0si1sn=iifn=00˙-˙TM×˙Tb0ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn=Tbi1-˙TM×˙Tbi
185 ovexd NFinRCRingMBsbB0si1sTbi1-˙TM×˙TbiV
186 9 184 108 185 fvmptd2 NFinRCRingMBsbB0si1sGi=Tbi1-˙TM×˙Tbi
187 186 oveq2d NFinRCRingMBsbB0si1si×˙X·˙Gi=i×˙X·˙Tbi1-˙TM×˙Tbi
188 187 mpteq2dva NFinRCRingMBsbB0si1si×˙X·˙Gi=i1si×˙X·˙Tbi1-˙TM×˙Tbi
189 188 oveq2d NFinRCRingMBsbB0sYi=1si×˙X·˙Gi=Yi=1si×˙X·˙Tbi1-˙TM×˙Tbi
190 nn0p1gt0 s00<s+1
191 0red s00
192 ltne 00<s+1s+10
193 191 192 sylan s00<s+1s+10
194 neeq1 n=s+1n0s+10
195 193 194 syl5ibrcom s00<s+1n=s+1n0
196 34 190 195 syl2anc2 sn=s+1n0
197 196 ad2antrl NFinRCRingMBsbB0sn=s+1n0
198 197 imp NFinRCRingMBsbB0sn=s+1n0
199 eqneqall n=0n00˙-˙TM×˙Tb0=Tbs
200 198 199 mpan9 NFinRCRingMBsbB0sn=s+1n=00˙-˙TM×˙Tb0=Tbs
201 iftrue n=s+1ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn=Tbs
202 201 ad2antlr NFinRCRingMBsbB0sn=s+1¬n=0ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn=Tbs
203 200 202 ifeqda NFinRCRingMBsbB0sn=s+1ifn=00˙-˙TM×˙Tb0ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn=Tbs
204 74 35 syl NFinRCRingMBsbB0ss+10
205 fvexd NFinRCRingMBsbB0sTbsV
206 9 203 204 205 fvmptd2 NFinRCRingMBsbB0sGs+1=Tbs
207 206 oveq2d NFinRCRingMBsbB0ss+1×˙X·˙Gs+1=s+1×˙X·˙Tbs
208 15 3ad2ant2 NFinRCRingMBRRing
209 eqid BaseP=BaseP
210 10 3 209 vr1cl RRingXBaseP
211 208 210 syl NFinRCRingMBXBaseP
212 eqid mulGrpP=mulGrpP
213 212 209 mgpbas BaseP=BasemulGrpP
214 eqid 1P=1P
215 212 214 ringidval 1P=0mulGrpP
216 213 215 12 mulg0 XBaseP0×˙X=1P
217 211 216 syl NFinRCRingMB0×˙X=1P
218 3 ply1crng RCRingPCRing
219 218 anim2i NFinRCRingNFinPCRing
220 219 3adant3 NFinRCRingMBNFinPCRing
221 4 matsca2 NFinPCRingP=ScalarY
222 220 221 syl NFinRCRingMBP=ScalarY
223 222 fveq2d NFinRCRingMB1P=1ScalarY
224 217 223 eqtrd NFinRCRingMB0×˙X=1ScalarY
225 224 adantr NFinRCRingMBsbB0s0×˙X=1ScalarY
226 225 oveq1d NFinRCRingMBsbB0s0×˙X·˙G0=1ScalarY·˙G0
227 3 4 pmatlmod NFinRRingYLMod
228 15 227 sylan2 NFinRCRingYLMod
229 228 3adant3 NFinRCRingMBYLMod
230 1 2 3 4 5 6 7 8 9 chfacfisf NFinRRingMBsbB0sG:0BaseY
231 15 230 syl3anl2 NFinRCRingMBsbB0sG:0BaseY
232 231 81 ffvelcdmd NFinRCRingMBsbB0sG0BaseY
233 eqid ScalarY=ScalarY
234 eqid 1ScalarY=1ScalarY
235 14 233 11 234 lmodvs1 YLModG0BaseY1ScalarY·˙G0=G0
236 229 232 235 syl2an2r NFinRCRingMBsbB0s1ScalarY·˙G0=G0
237 iftrue n=0ifn=00˙-˙TM×˙Tb0ifn=s+1Tbsifs+1<n0˙Tbn1-˙TM×˙Tbn=0˙-˙TM×˙Tb0
238 ovexd NFinRCRingMBsbB0s0˙-˙TM×˙Tb0V
239 9 237 81 238 fvmptd3 NFinRCRingMBsbB0sG0=0˙-˙TM×˙Tb0
240 226 236 239 3eqtrd NFinRCRingMBsbB0s0×˙X·˙G0=0˙-˙TM×˙Tb0
241 207 240 oveq12d NFinRCRingMBsbB0ss+1×˙X·˙Gs+1+˙0×˙X·˙G0=s+1×˙X·˙Tbs+˙0˙-˙TM×˙Tb0
242 14 13 cmncom YCMnd0×˙X·˙G0BaseYs+1×˙X·˙Gs+1BaseY0×˙X·˙G0+˙s+1×˙X·˙Gs+1=s+1×˙X·˙Gs+1+˙0×˙X·˙G0
243 22 83 96 242 syl3anc NFinRCRingMBsbB0s0×˙X·˙G0+˙s+1×˙X·˙Gs+1=s+1×˙X·˙Gs+1+˙0×˙X·˙G0
244 ringgrp YRingYGrp
245 19 244 syl NFinRCRingMBYGrp
246 245 adantr NFinRCRingMBsbB0sYGrp
247 207 96 eqeltrrd NFinRCRingMBsbB0ss+1×˙X·˙TbsBaseY
248 19 adantr NFinRCRingMBsbB0sYRing
249 8 1 2 3 4 mat2pmatbas NFinRRingMBTMBaseY
250 15 249 syl3an2 NFinRCRingMBTMBaseY
251 250 adantr NFinRCRingMBsbB0sTMBaseY
252 simpl1 NFinRCRingMBsbB0sNFin
253 208 adantr NFinRCRingMBsbB0sRRing
254 elmapi bB0sb:0sB
255 254 adantl sbB0sb:0sB
256 255 adantl NFinRCRingMBsbB0sb:0sB
257 0elfz s000s
258 34 257 syl s00s
259 258 ad2antrl NFinRCRingMBsbB0s00s
260 256 259 ffvelcdmd NFinRCRingMBsbB0sb0B
261 8 1 2 3 4 mat2pmatbas NFinRRingb0BTb0BaseY
262 252 253 260 261 syl3anc NFinRCRingMBsbB0sTb0BaseY
263 14 5 ringcl YRingTMBaseYTb0BaseYTM×˙Tb0BaseY
264 248 251 262 263 syl3anc NFinRCRingMBsbB0sTM×˙Tb0BaseY
265 14 7 6 13 grpsubadd0sub YGrps+1×˙X·˙TbsBaseYTM×˙Tb0BaseYs+1×˙X·˙Tbs-˙TM×˙Tb0=s+1×˙X·˙Tbs+˙0˙-˙TM×˙Tb0
266 246 247 264 265 syl3anc NFinRCRingMBsbB0ss+1×˙X·˙Tbs-˙TM×˙Tb0=s+1×˙X·˙Tbs+˙0˙-˙TM×˙Tb0
267 241 243 266 3eqtr4d NFinRCRingMBsbB0s0×˙X·˙G0+˙s+1×˙X·˙Gs+1=s+1×˙X·˙Tbs-˙TM×˙Tb0
268 189 267 oveq12d NFinRCRingMBsbB0sYi=1si×˙X·˙Gi+˙0×˙X·˙G0+˙s+1×˙X·˙Gs+1=Yi=1si×˙X·˙Tbi1-˙TM×˙Tbi+˙s+1×˙X·˙Tbs-˙TM×˙Tb0
269 113 268 eqtrd NFinRCRingMBsbB0sYi=1si×˙X·˙Gi+˙0×˙X·˙G0+˙s+1×˙X·˙Gs+1=Yi=1si×˙X·˙Tbi1-˙TM×˙Tbi+˙s+1×˙X·˙Tbs-˙TM×˙Tb0
270 75 102 269 3eqtrd NFinRCRingMBsbB0sYi=0s+1i×˙X·˙Gi=Yi=1si×˙X·˙Tbi1-˙TM×˙Tbi+˙s+1×˙X·˙Tbs-˙TM×˙Tb0
271 40 73 270 3eqtrd NFinRCRingMBsbB0sYi0i×˙X·˙Gi=Yi=1si×˙X·˙Tbi1-˙TM×˙Tbi+˙s+1×˙X·˙Tbs-˙TM×˙Tb0