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

Theorem monmat2matmon 19108
 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 crngrng 17005 . . 3
2 simpll 753 . . . . 5
3 simplr 754 . . . . 5
4 monmat2matmon.a . . . . . 6 Mat
5 monmat2matmon.k . . . . . 6
6 monmat2matmon.t . . . . . 6 matToPolyMat
7 monmat2matmon.p . . . . . 6 Poly1
8 monmat2matmon.c . . . . . 6 Mat
9 monmat2matmon.b . . . . . 6
10 monmat2matmon.m2 . . . . . 6
11 monmat2matmon.e2 . . . . . 6 .gmulGrp
12 monmat2matmon.y . . . . . 6 var1
134, 5, 6, 7, 8, 9, 10, 11, 12mat2pmatscmxcl 19024 . . . . 5
142, 3, 133jca 1176 . . . 4
15 monmat2matmon.m1 . . . . 5
16 monmat2matmon.e1 . . . . 5 .gmulGrp
17 monmat2matmon.x . . . . 5 var1
18 monmat2matmon.q . . . . 5 Poly1
19 monmat2matmon.i . . . . 5 pMatToMatPoly
207, 8, 9, 15, 16, 17, 4, 18, 19pm2mpfval 19080 . . . 4 g decompPMat
2114, 20syl 16 . . 3 g decompPMat
221, 21sylanl2 651 . 2 g decompPMat
23 simpll 753 . . . . . . . 8
24 simpr 461 . . . . . . . . . 10
2524anim1i 568 . . . . . . . . 9
26 df-3an 975 . . . . . . . . 9
2725, 26sylibr 212 . . . . . . . 8
28 eqid 2467 . . . . . . . . 9
297, 8, 4, 5, 28, 11, 12, 10, 6monmatcollpw 19063 . . . . . . . 8 decompPMat
3023, 27, 29syl2anc 661 . . . . . . 7 decompPMat
3130oveq1d 6298 . . . . . 6 decompPMat
321a1i 11 . . . . . . . . . 10
3332anim2d 565 . . . . . . . . 9
3433anim1d 564 . . . . . . . 8
3534imdistanri 691 . . . . . . 7
36 ovif 6362 . . . . . . . 8
374matrng 18728 . . . . . . . . . . . . . 14
3818ply1sca 18081 . . . . . . . . . . . . . 14 Scalar
3937, 38syl 16 . . . . . . . . . . . . 13 Scalar
4039ad2antrr 725 . . . . . . . . . . . 12 Scalar
4140fveq2d 5869 . . . . . . . . . . 11 Scalar
4241oveq1d 6298 . . . . . . . . . 10 Scalar
4318ply1lmod 18080 . . . . . . . . . . . . 13
4437, 43syl 16 . . . . . . . . . . . 12
4544ad2antrr 725 . . . . . . . . . . 11
4618ply1rng 18076 . . . . . . . . . . . . . . 15
4737, 46syl 16 . . . . . . . . . . . . . 14
48 eqid 2467 . . . . . . . . . . . . . . 15 mulGrp mulGrp
4948rngmgp 17001 . . . . . . . . . . . . . 14 mulGrp
5047, 49syl 16 . . . . . . . . . . . . 13 mulGrp
5150ad2antrr 725 . . . . . . . . . . . 12 mulGrp
52 simpr 461 . . . . . . . . . . . 12
53 eqid 2467 . . . . . . . . . . . . . . 15
5417, 18, 53vr1cl 18045 . . . . . . . . . . . . . 14
5537, 54syl 16 . . . . . . . . . . . . 13
5655ad2antrr 725 . . . . . . . . . . . 12
5748, 53mgpbas 16946 . . . . . . . . . . . . 13 mulGrp
5857, 16mulgnn0cl 15965 . . . . . . . . . . . 12 mulGrp
5951, 52, 56, 58syl3anc 1228 . . . . . . . . . . 11
60 eqid 2467 . . . . . . . . . . . 12 Scalar Scalar
61 eqid 2467 . . . . . . . . . . . 12 Scalar Scalar
62 eqid 2467 . . . . . . . . . . . 12
6353, 60, 15, 61, 62lmod0vs 17340 . . . . . . . . . . 11 Scalar
6445, 59, 63syl2anc 661 . . . . . . . . . 10 Scalar
6542, 64eqtrd 2508 . . . . . . . . 9
6665ifeq2d 3958 . . . . . . . 8
6736, 66syl5eq 2520 . . . . . . 7
6835, 67syl 16 . . . . . 6
6931, 68eqtrd 2508 . . . . 5 decompPMat
7069mpteq2dva 4533 . . . 4 decompPMat
7170oveq2d 6299 . . 3 g decompPMat g
72 rngmnd 17004 . . . . . . 7
7347, 72syl 16 . . . . . 6
7473adantr 465 . . . . 5
75 nn0ex 10800 . . . . . 6
7675a1i 11 . . . . 5
77 simprr 756 . . . . 5
78 eqid 2467 . . . . 5
7939fveq2d 5869 . . . . . . . . . . . . 13 Scalar
805, 79syl5eq 2520 . . . . . . . . . . . 12 Scalar
8180eleq2d 2537 . . . . . . . . . . 11 Scalar
8281biimpcd 224 . . . . . . . . . 10 Scalar
8382adantr 465 . . . . . . . . 9 Scalar
8483impcom 430 . . . . . . . 8 Scalar
8584adantr 465 . . . . . . 7 Scalar
86 eqid 2467 . . . . . . . 8 Scalar Scalar
8753, 60, 15, 86lmodvscl 17324 . . . . . . 7 Scalar
8845, 85, 59, 87syl3anc 1228 . . . . . 6
8988ralrimiva 2878 . . . . 5
9062, 74, 76, 77, 78, 89gsummpt1n0 16792 . . . 4 g
911, 90sylanl2 651 . . 3 g
9271, 91eqtrd 2508 . 2 g decompPMat
93 csbov2g 6319 . . . 4
94 csbov1g 6318 . . . . . 6
95 csbvarg 3848 . . . . . . 7
9695oveq1d 6298 . . . . . 6
9794, 96eqtrd 2508 . . . . 5
9897oveq2d 6299 . . . 4
9993, 98eqtrd 2508 . . 3