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

Theorem monmat2matmon 19848
 Description: The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-Nov-2019.) (Revised by AV, 7-Dec-2019.)
Hypotheses
Ref Expression
monmat2matmon.p Poly1
monmat2matmon.c Mat
monmat2matmon.b
monmat2matmon.m1
monmat2matmon.e1 .gmulGrp
monmat2matmon.x var1
monmat2matmon.a Mat
monmat2matmon.k
monmat2matmon.q Poly1
monmat2matmon.i pMatToMatPoly
monmat2matmon.e2 .gmulGrp
monmat2matmon.y var1
monmat2matmon.m2
monmat2matmon.t matToPolyMat
Assertion
Ref Expression
monmat2matmon

Proof of Theorem monmat2matmon
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 crngring 17791 . . 3
2 simpll 760 . . . 4
3 simplr 762 . . . 4
4 monmat2matmon.a . . . . 5 Mat
5 monmat2matmon.k . . . . 5
6 monmat2matmon.t . . . . 5 matToPolyMat
7 monmat2matmon.p . . . . 5 Poly1
8 monmat2matmon.c . . . . 5 Mat
9 monmat2matmon.b . . . . 5
10 monmat2matmon.m2 . . . . 5
11 monmat2matmon.e2 . . . . 5 .gmulGrp
12 monmat2matmon.y . . . . 5 var1
134, 5, 6, 7, 8, 9, 10, 11, 12mat2pmatscmxcl 19764 . . . 4
14 monmat2matmon.m1 . . . . 5
15 monmat2matmon.e1 . . . . 5 .gmulGrp
16 monmat2matmon.x . . . . 5 var1
17 monmat2matmon.q . . . . 5 Poly1
18 monmat2matmon.i . . . . 5 pMatToMatPoly
197, 8, 9, 14, 15, 16, 4, 17, 18pm2mpfval 19820 . . . 4 g decompPMat
202, 3, 13, 19syl3anc 1268 . . 3 g decompPMat
211, 20sylanl2 657 . 2 g decompPMat
22 simpll 760 . . . . . . . 8
23 simpr 463 . . . . . . . . . 10
2423anim1i 572 . . . . . . . . 9
25 df-3an 987 . . . . . . . . 9
2624, 25sylibr 216 . . . . . . . 8
27 eqid 2451 . . . . . . . . 9
287, 8, 4, 5, 27, 11, 12, 10, 6monmatcollpw 19803 . . . . . . . 8 decompPMat
2922, 26, 28syl2anc 667 . . . . . . 7 decompPMat
3029oveq1d 6305 . . . . . 6 decompPMat
311a1i 11 . . . . . . . . . 10
3231anim2d 569 . . . . . . . . 9
3332anim1d 568 . . . . . . . 8
3433imdistanri 697 . . . . . . 7
35 ovif 6373 . . . . . . . 8
364matring 19468 . . . . . . . . . . . . . 14
3717ply1sca 18846 . . . . . . . . . . . . . 14 Scalar
3836, 37syl 17 . . . . . . . . . . . . 13 Scalar
3938ad2antrr 732 . . . . . . . . . . . 12 Scalar
4039fveq2d 5869 . . . . . . . . . . 11 Scalar
4140oveq1d 6305 . . . . . . . . . 10 Scalar
4217ply1lmod 18845 . . . . . . . . . . . . 13
4336, 42syl 17 . . . . . . . . . . . 12
4443ad2antrr 732 . . . . . . . . . . 11
4517ply1ring 18841 . . . . . . . . . . . . . . 15
4636, 45syl 17 . . . . . . . . . . . . . 14
47 eqid 2451 . . . . . . . . . . . . . . 15 mulGrp mulGrp
4847ringmgp 17786 . . . . . . . . . . . . . 14 mulGrp
4946, 48syl 17 . . . . . . . . . . . . 13 mulGrp
5049ad2antrr 732 . . . . . . . . . . . 12 mulGrp
51 simpr 463 . . . . . . . . . . . 12
52 eqid 2451 . . . . . . . . . . . . . . 15
5316, 17, 52vr1cl 18810 . . . . . . . . . . . . . 14
5436, 53syl 17 . . . . . . . . . . . . 13
5554ad2antrr 732 . . . . . . . . . . . 12
5647, 52mgpbas 17729 . . . . . . . . . . . . 13 mulGrp
5756, 15mulgnn0cl 16774 . . . . . . . . . . . 12 mulGrp
5850, 51, 55, 57syl3anc 1268 . . . . . . . . . . 11
59 eqid 2451 . . . . . . . . . . . 12 Scalar Scalar
60 eqid 2451 . . . . . . . . . . . 12 Scalar Scalar
61 eqid 2451 . . . . . . . . . . . 12
6252, 59, 14, 60, 61lmod0vs 18124 . . . . . . . . . . 11 Scalar
6344, 58, 62syl2anc 667 . . . . . . . . . 10 Scalar
6441, 63eqtrd 2485 . . . . . . . . 9
6564ifeq2d 3900 . . . . . . . 8
6635, 65syl5eq 2497 . . . . . . 7
6734, 66syl 17 . . . . . 6
6830, 67eqtrd 2485 . . . . 5 decompPMat
6968mpteq2dva 4489 . . . 4 decompPMat
7069oveq2d 6306 . . 3 g decompPMat g
71 ringmnd 17789 . . . . . . 7
7246, 71syl 17 . . . . . 6
7372adantr 467 . . . . 5
74 nn0ex 10875 . . . . . 6
7574a1i 11 . . . . 5
76 simprr 766 . . . . 5
77 eqid 2451 . . . . 5
7838fveq2d 5869 . . . . . . . . . . . . 13 Scalar
795, 78syl5eq 2497 . . . . . . . . . . . 12 Scalar
8079eleq2d 2514 . . . . . . . . . . 11 Scalar
8180biimpcd 228 . . . . . . . . . 10 Scalar
8281adantr 467 . . . . . . . . 9 Scalar
8382impcom 432 . . . . . . . 8 Scalar
8483adantr 467 . . . . . . 7 Scalar
85 eqid 2451 . . . . . . . 8 Scalar Scalar
8652, 59, 14, 85lmodvscl 18108 . . . . . . 7 Scalar
8744, 84, 58, 86syl3anc 1268 . . . . . 6
8887ralrimiva 2802 . . . . 5
8961, 73, 75, 76, 77, 88gsummpt1n0 17597 . . . 4 g
901, 89sylanl2 657 . . 3 g
9170, 90eqtrd 2485 . 2 g decompPMat
92 csbov2g 6328 . . . 4
93 csbov1g 6327 . . . . . 6
94 csbvarg 3792 . . . . . . 7
9594oveq1d 6305 . . . . . 6
9693, 95eqtrd 2485 . . . . 5
9796oveq2d 6306 . . . 4
9892, 97eqtrd 2485 . . 3