Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  chfacfpmmulgsum Structured version   Unicode version

Theorem chfacfpmmulgsum 19492
 Description: Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.)
Hypotheses
Ref Expression
cayhamlem1.a Mat
cayhamlem1.b
cayhamlem1.p Poly1
cayhamlem1.y Mat
cayhamlem1.r
cayhamlem1.s
cayhamlem1.0
cayhamlem1.t matToPolyMat
cayhamlem1.g
cayhamlem1.e .gmulGrp
chfacfpmmulgsum.p
Assertion
Ref Expression
chfacfpmmulgsum g g
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,,   ,   ,   ,
Allowed substitution hints:   (,,,)   (,)   (,,,)   (,,,)   (,)   (,)   (,)   (,,)   (,,)   (,)   (,,)   (,)   (,)   (,,)

Proof of Theorem chfacfpmmulgsum
StepHypRef Expression
1 eqid 2457 . . 3
2 cayhamlem1.0 . . 3
3 chfacfpmmulgsum.p . . 3
4 crngring 17336 . . . . . . . 8
54anim2i 569 . . . . . . 7
653adant3 1016 . . . . . 6
7 cayhamlem1.p . . . . . . 7 Poly1
8 cayhamlem1.y . . . . . . 7 Mat
97, 8pmatring 19321 . . . . . 6
106, 9syl 16 . . . . 5
11 ringcmn 17356 . . . . 5 CMnd
1210, 11syl 16 . . . 4 CMnd
1312adantr 465 . . 3 CMnd
14 nn0ex 10822 . . . 4
1514a1i 11 . . 3
16 simpll 753 . . . . 5
17 simplr 755 . . . . 5
18 simpr 461 . . . . 5
1916, 17, 183jca 1176 . . . 4
20 cayhamlem1.a . . . . 5 Mat
21 cayhamlem1.b . . . . 5
22 cayhamlem1.r . . . . 5
23 cayhamlem1.s . . . . 5
24 cayhamlem1.t . . . . 5 matToPolyMat
25 cayhamlem1.g . . . . 5
26 cayhamlem1.e . . . . 5 .gmulGrp
2720, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19489 . . . 4
2819, 27syl 16 . . 3
2920, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulfsupp 19491 . . 3 finSupp
30 nn0disj 11817 . . . 4
3130a1i 11 . . 3
32 nnnn0 10823 . . . . . 6
33 peano2nn0 10857 . . . . . 6
3432, 33syl 16 . . . . 5
35 nn0split 11816 . . . . 5
3634, 35syl 16 . . . 4
381, 2, 3, 13, 15, 28, 29, 31, 37gsumsplit2 17075 . 2 g g g
39 simpll 753 . . . . . . . 8
40 simplr 755 . . . . . . . 8
41 nncn 10564 . . . . . . . . . . . . 13
42 add1p1 10809 . . . . . . . . . . . . 13
4341, 42syl 16 . . . . . . . . . . . 12
4443ad2antrl 727 . . . . . . . . . . 11
4544fveq2d 5876 . . . . . . . . . 10
4645eleq2d 2527 . . . . . . . . 9
4746biimpa 484 . . . . . . . 8
4820, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmul0 19490 . . . . . . . 8
4939, 40, 47, 48syl3anc 1228 . . . . . . 7
5049mpteq2dva 4543 . . . . . 6
5150oveq2d 6312 . . . . 5 g g
524, 9sylan2 474 . . . . . . . . . 10
53 ringmnd 17334 . . . . . . . . . 10
5452, 53syl 16 . . . . . . . . 9
55543adant3 1016 . . . . . . . 8
56 fvex 5882 . . . . . . . 8
5755, 56jctir 538 . . . . . . 7
5857adantr 465 . . . . . 6
592gsumz 16132 . . . . . 6 g
6058, 59syl 16 . . . . 5 g
6151, 60eqtrd 2498 . . . 4 g
6261oveq2d 6312 . . 3 g g g
6355adantr 465 . . . 4
64 fzfid 12086 . . . . 5
65 elfznn0 11797 . . . . . . . 8
6665, 19sylan2 474 . . . . . . 7
6766, 27syl 16 . . . . . 6
6867ralrimiva 2871 . . . . 5
691, 13, 64, 68gsummptcl 17121 . . . 4 g
701, 3, 2mndrid 16069 . . . 4 g g g
7163, 69, 70syl2anc 661 . . 3 g g
7262, 71eqtrd 2498 . 2 g g g
7332ad2antrl 727 . . . 4
741, 3, 13, 73, 67gsummptfzsplit 17079 . . 3 g g g
75 elfznn0 11797 . . . . . . 7
7675, 28sylan2 474 . . . . . 6
771, 3, 13, 73, 76gsummptfzsplitl 17080 . . . . 5 g g g
78 0nn0 10831 . . . . . . . 8
7978a1i 11 . . . . . . 7
8020, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19489 . . . . . . . 8
8179, 80mpd3an3 1325 . . . . . . 7
82 oveq1 6303 . . . . . . . . 9
83 fveq2 5872 . . . . . . . . 9
8482, 83oveq12d 6314 . . . . . . . 8
851, 84gsumsn 17108 . . . . . . 7 g
8663, 79, 81, 85syl3anc 1228 . . . . . 6 g
8786oveq2d 6312 . . . . 5 g g g
8877, 87eqtrd 2498 . . . 4 g g
89 ovex 6324 . . . . . 6
9089a1i 11 . . . . 5
91 1nn0 10832 . . . . . . . 8
9291a1i 11 . . . . . . 7
9373, 92nn0addcld 10877 . . . . . 6
9420, 21, 7, 8, 22, 23, 2, 24, 25, 26chfacfpmmulcl 19489 . . . . . 6
9593, 94mpd3an3 1325 . . . . 5
96 oveq1 6303 . . . . . . 7
97 fveq2 5872 . . . . . . 7
9896, 97oveq12d 6314 . . . . . 6
991, 98gsumsn 17108 . . . . 5 g
10063, 90, 95, 99syl3anc 1228 . . . 4 g
10188, 100oveq12d 6314 . . 3 g g g
102 fzfid 12086 . . . . . 6
103 simpll 753 . . . . . . . 8
104 simplr 755 . . . . . . . 8
105 elfznn 11739 . . . . . . . . . 10
106105nnnn0d 10873 . . . . . . . . 9
107106adantl 466 . . . . . . . 8
108103, 104, 107, 27syl3anc 1228 . . . . . . 7
109108ralrimiva 2871 . . . . . 6
1101, 13, 102, 109gsummptcl 17121 . . . . 5 g
1111, 3mndass 16057 . . . . 5 g g g
11263, 110, 81, 95, 111syl13anc 1230 . . . 4 g g
11325a1i 11 . . . . . . . . 9
114105nnne0d 10601 . . . . . . . . . . . . . 14
115114ad2antlr 726 . . . . . . . . . . . . 13
116 neeq1 2738 . . . . . . . . . . . . . 14
117116adantl 466 . . . . . . . . . . . . 13
118115, 117mpbird 232 . . . . . . . . . . . 12
119 eqneqall 2664 . . . . . . . . . . . 12
120118, 119mpan9 469 . . . . . . . . . . 11
121 simplr 755 . . . . . . . . . . . . . . 15
122 eqeq1 2461 . . . . . . . . . . . . . . . . 17
123122eqcoms 2469 . . . . . . . . . . . . . . . 16
124123adantl 466 . . . . . . . . . . . . . . 15
125121, 124mpbird 232 . . . . . . . . . . . . . 14
126125fveq2d 5876 . . . . . . . . . . . . 13
127126fveq2d 5876 . . . . . . . . . . . 12
128127oveq2d 6312 . . . . . . . . . . 11
129120, 128oveq12d 6314 . . . . . . . . . 10
130 elfz2 11704 . . . . . . . . . . . . . . . . . 18
131 zleltp1 10935 . . . . . . . . . . . . . . . . . . . . . . . . 25
132131ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . 24
1331323adant1 1014 . . . . . . . . . . . . . . . . . . . . . . 23
134133biimpcd 224 . . . . . . . . . . . . . . . . . . . . . 22
135134adantl 466 . . . . . . . . . . . . . . . . . . . . 21
136135impcom 430 . . . . . . . . . . . . . . . . . . . 20
137136orcd 392 . . . . . . . . . . . . . . . . . . 19
138 zre 10889 . . . . . . . . . . . . . . . . . . . . . . . 24
139 1red 9628 . . . . . . . . . . . . . . . . . . . . . . . 24
140138, 139readdcld 9640 . . . . . . . . . . . . . . . . . . . . . . 23
141 zre 10889 . . . . . . . . . . . . . . . . . . . . . . 23
142140, 141anim12ci 567 . . . . . . . . . . . . . . . . . . . . . 22
1431423adant1 1014 . . . . . . . . . . . . . . . . . . . . 21
144 lttri2 9684 . . . . . . . . . . . . . . . . . . . . 21
145143, 144syl 16 . . . . . . . . . . . . . . . . . . . 20
146145adantr 465 . . . . . . . . . . . . . . . . . . 19
147137, 146mpbird 232 . . . . . . . . . . . . . . . . . 18
148130, 147sylbi 195 . . . . . . . . . . . . . . . . 17
149148ad2antlr 726 . . . . . . . . . . . . . . . 16
150 neeq1 2738 . . . . . . . . . . . . . . . . 17
151150adantl 466 . . . . . . . . . . . . . . . 16
152149, 151mpbird 232 . . . . . . . . . . . . . . 15
153152adantr 465 . . . . . . . . . . . . . 14
154153neneqd 2659 . . . . . . . . . . . . 13
155154pm2.21d 106 . . . . . . . . . . . 12
156155imp 429 . . . . . . . . . . 11
157105nnred 10571 . . . . . . . . . . . . . . . . . . 19
158 eleq1 2529 . . . . . . . . . . . . . . . . . . 19
159157, 158syl5ibrcom 222 . . . . . . . . . . . . . . . . . 18
160159adantl 466 . . . . . . . . . . . . . . . . 17
161160imp 429 . . . . . . . . . . . . . . . 16
16273nn0red 10874 . . . . . . . . . . . . . . . . . 18
163162ad2antrr 725 . . . . . . . . . . . . . . . . 17
164 1red 9628 . . . . . . . . . . . . . . . . 17
165163, 164readdcld 9640 . . . . . . . . . . . . . . . 16
166130, 136sylbi 195 . . . . . . . . . . . . . . . . . 18
167166ad2antlr 726 . . . . . . . . . . . . . . . . 17
168 breq1 4459 . . . . . . . . . . . . . . . . . 18
169168adantl 466 . . . . . . . . . . . . . . . . 17
170167, 169mpbird 232 . . . . . . . . . . . . . . . 16
171161, 165, 170ltnsymd 9751 . . . . . . . . . . . . . . 15
172171pm2.21d 106 . . . . . . . . . . . . . 14
173172ad2antrr 725 . . . . . . . . . . . . 13
174173imp 429 . . . . . . . . . . . 12
175 simp-4r 768 . . . . . . . . . . . . . . . 16
176175oveq1d 6311 . . . . . . . . . . . . . . 15
177176fveq2d 5876 . . . . . . . . . . . . . 14
178177fveq2d 5876 . . . . . . . . . . . . 13
179175fveq2d 5876 . . . . . . . . . . . . . . 15
180179fveq2d 5876 . . . . . . . . . . . . . 14
181180oveq2d 6312 . . . . . . . . . . . . 13
182178, 181oveq12d 6314 . . . . . . . . . . . 12
183174, 182ifeqda 3977 . . . . . . . . . . 11
184156, 183ifeqda 3977 . . . . . . . . . 10
185129, 184ifeqda 3977 . . . . . . . . 9
186 ovex 6324 . . . . . . . . . 10
187186a1i 11 . . . . . . . . 9
188113, 185, 107, 187fvmptd 5961 . . . . . . . 8
189188oveq2d 6312 . . . . . . 7
190189mpteq2dva 4543 . . . . . 6
191190oveq2d 6312 . . . . 5 g g
19225a1i 11 . . . . . . . . 9
193 nn0p1gt0 10846 . . . . . . . . . . . . . . 15
194 0red 9614 . . . . . . . . . . . . . . . . 17
195 ltne 9698 . . . . . . . . . . . . . . . . 17
196194, 195sylan 471 . . . . . . . . . . . . . . . 16
197 neeq1 2738 . . . . . . . . . . . . . . . 16
198196, 197syl5ibrcom 222 . . . . . . . . . . . . . . 15
199193, 198mpdan 668 . . . . . . . . . . . . . 14
20032, 199syl 16 . . . . . . . . . . . . 13
201200ad2antrl 727 . . . . . . . . . . . 12
202201imp 429 . . . . . . . . . . 11
203 eqneqall 2664 . . . . . . . . . . 11
204202, 203mpan9 469 . . . . . . . . . 10
205 iftrue 3950 . . . . . . . . . . 11
206205ad2antlr 726 . . . . . . . . . 10
207204, 206ifeqda 3977 . . . . . . . . 9
20873, 33syl 16 . . . . . . . . 9
209 fvex 5882 . . . . . . . . . 10
210209a1i 11 . . . . . . . . 9
211192, 207, 208, 210fvmptd 5961 . . . . . . . 8
212211oveq2d 6312 . . . . . . 7
21324, 20, 21, 7, 8mat2pmatbas 19354 . . . . . . . . . . . . 13
2144, 213syl3an2 1262 . . . . . . . . . . . 12
215 eqid 2457 . . . . . . . . . . . . . 14 mulGrp mulGrp
216215, 1mgpbas 17274 . . . . . . . . . . . . 13 mulGrp
217 eqid 2457 . . . . . . . . . . . . 13 mulGrp mulGrp
218216, 217, 26mulg0 16274 . . . . . . . . . . . 12 mulGrp
219214, 218syl 16 . . . . . . . . . . 11 mulGrp
220 eqid 2457 . . . . . . . . . . . 12
221215, 220ringidval 17282 . . . . . . . . . . 11 mulGrp
222219, 221syl6eqr 2516 . . . . . . . . . 10
223222adantr 465 . . . . . . . . 9
224223oveq1d 6311 . . . . . . . 8
225523adant3 1016 . . . . . . . . . 10
226225adantr 465 . . . . . . . . 9
22720, 21, 7, 8, 22, 23, 2, 24, 25chfacfisf 19482 . . . . . . . . . . 11
2284, 227syl3anl2 1277 . . . . . . . . . 10
229228, 79ffvelrnd 6033 . . . . . . . . 9
2301, 22, 220ringlidm 17349 . . . . . . . . 9
231226, 229, 230syl2anc 661 . . . . . . . 8
232 iftrue 3950 . . . . . . . . . 10
233232adantl 466 . . . . . . . . 9
234 ovex 6324 . . . . . . . . . 10
235234a1i 11 . . . . . . . . 9
236192, 233, 79, 235fvmptd 5961 . . . . . . . 8
237224, 231, 2363eqtrd 2502 . . . . . . 7
238212, 237oveq12d 6314 . . . . . 6
2391, 3cmncom 16941 . . . . . . 7 CMnd
24013, 81, 95, 239syl3anc 1228 . . . . . 6
241 ringgrp 17330 . . . . . . . . 9
24210, 241syl 16 . . . . . . . 8
243242adantr 465 . . . . . . 7
244212, 95eqeltrrd 2546 . . . . . . 7
24510adantr 465 . . . . . . . 8
246214adantr 465 . . . . . . . 8
247 simpl1 999 . . . . . . . . 9
24843ad2ant2 1018 . . . . . . . . . 10
249248adantr 465 . . . . . . . . 9
250 elmapi 7459 . . . . . . . . . . . 12
251250adantl 466 . . . . . . . . . . 11
252251adantl 466 . . . . . . . . . 10
253 0elfz 11799 . . . . . . . . . . . 12
25432, 253syl 16 . . . . . . . . . . 11
255254ad2antrl 727 . . . . . . . . . 10
256252, 255ffvelrnd 6033 . . . . . . . . 9
25724, 20, 21, 7, 8mat2pmatbas 19354 . . . . . . . . 9
258247, 249, 256, 257syl3anc 1228 . . . . . . . 8
2591, 22ringcl 17339 . . . . . . . 8
260245, 246, 258, 259syl3anc 1228 . . . . . . 7
2611, 2, 23, 3grpsubadd0sub 16252 . . . . . . 7
262243, 244, 260, 261syl3anc 1228 . . . . . 6
263238, 240, 2623eqtr4d 2508 . . . . 5
264191, 263oveq12d 6314 . . . 4 g g
265112, 264eqtrd 2498 . . 3 g g
26674, 101, 2653eqtrd 2502 . 2 g g
26738, 72, 2663eqtrd 2502 1 g g
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wo 368   wa 369   w3a 973   wceq 1395   wcel 1819   wne 2652  cvv 3109   cun 3469   cin 3470  c0 3793  cif 3944  csn 4032   class class class wbr 4456   cmpt 4515  wf 5590  cfv 5594  (class class class)co 6296   cmap 7438  cfn 7535  cc 9507  cr 9508  cc0 9509  c1 9510   caddc 9512   clt 9645   cle 9646   cmin 9824  cn 10556  c2 10606  cn0 10816  cz 10885  cuz 11106  cfz 11697  cbs 14644   cplusg 14712  cmulr 14713  c0g 14857   g cgsu 14858  cmnd 16046  cgrp 16180  csg 16182  .gcmg 16183  CMndccmn 16925  mulGrpcmgp 17268  cur 17280  crg 17325  ccrg 17326  Poly1cpl1 18343   Mat cmat 19036   matToPolyMat cmat2pmat 19332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow