Metamath Proof Explorer

Theorem monmat2matmon

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)

Ref Expression
Hypotheses monmat2matmon.p 
|- P = ( Poly1 ` R )
monmat2matmon.c 
|- C = ( N Mat P )
monmat2matmon.b 
|- B = ( Base ` C )
monmat2matmon.m1 
|- .* = ( .s ` Q )
monmat2matmon.e1 
|- .^ = ( .g ` ( mulGrp ` Q ) )
monmat2matmon.x 
|- X = ( var1 ` A )
monmat2matmon.a 
|- A = ( N Mat R )
monmat2matmon.k 
|- K = ( Base ` A )
monmat2matmon.q 
|- Q = ( Poly1 ` A )
monmat2matmon.i 
|- I = ( N pMatToMatPoly R )
monmat2matmon.e2 
|- E = ( .g ` ( mulGrp ` P ) )
monmat2matmon.y 
|- Y = ( var1 ` R )
monmat2matmon.m2 
|- .x. = ( .s ` C )
monmat2matmon.t 
|- T = ( N matToPolyMat R )
Assertion monmat2matmon 
|- ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( I ` ( ( L E Y ) .x. ( T ` M ) ) ) = ( M .* ( L .^ X ) ) )

Proof

Step Hyp Ref Expression
1 monmat2matmon.p 
 |-  P = ( Poly1 ` R )
2 monmat2matmon.c 
 |-  C = ( N Mat P )
3 monmat2matmon.b 
 |-  B = ( Base ` C )
4 monmat2matmon.m1 
 |-  .* = ( .s ` Q )
5 monmat2matmon.e1 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 monmat2matmon.x 
 |-  X = ( var1 ` A )
7 monmat2matmon.a 
 |-  A = ( N Mat R )
8 monmat2matmon.k 
 |-  K = ( Base ` A )
9 monmat2matmon.q 
 |-  Q = ( Poly1 ` A )
10 monmat2matmon.i 
 |-  I = ( N pMatToMatPoly R )
11 monmat2matmon.e2 
 |-  E = ( .g ` ( mulGrp ` P ) )
12 monmat2matmon.y 
 |-  Y = ( var1 ` R )
13 monmat2matmon.m2 
 |-  .x. = ( .s ` C )
14 monmat2matmon.t 
 |-  T = ( N matToPolyMat R )
15 crngring 
 |-  ( R e. CRing -> R e. Ring )
16 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> N e. Fin )
17 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> R e. Ring )
18 7 8 14 1 2 3 13 11 12 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( ( L E Y ) .x. ( T ` M ) ) e. B )
19 1 2 3 4 5 6 7 9 10 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( ( L E Y ) .x. ( T ` M ) ) e. B ) -> ( I ` ( ( L E Y ) .x. ( T ` M ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) ) ) )
20 16 17 18 19 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( I ` ( ( L E Y ) .x. ( T ` M ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) ) ) )
21 15 20 sylanl2 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( I ` ( ( L E Y ) .x. ( T ` M ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) ) ) )
22 simpll 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( N e. Fin /\ R e. CRing ) )
23 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( M e. K /\ L e. NN0 ) )
24 23 anim1i 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( M e. K /\ L e. NN0 ) /\ k e. NN0 ) )
25 df-3an 
 |-  ( ( M e. K /\ L e. NN0 /\ k e. NN0 ) <-> ( ( M e. K /\ L e. NN0 ) /\ k e. NN0 ) )
26 24 25 sylibr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( M e. K /\ L e. NN0 /\ k e. NN0 ) )
27 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
28 1 2 7 8 27 11 12 13 14 monmatcollpw 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 /\ k e. NN0 ) ) -> ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) = if ( k = L , M , ( 0g ` A ) ) )
29 22 26 28 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) = if ( k = L , M , ( 0g ` A ) ) )
30 29 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) = ( if ( k = L , M , ( 0g ` A ) ) .* ( k .^ X ) ) )
31 15 a1i 
 |-  ( k e. NN0 -> ( R e. CRing -> R e. Ring ) )
32 31 anim2d 
 |-  ( k e. NN0 -> ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) ) )
33 32 anim1d 
 |-  ( k e. NN0 -> ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) ) )
34 33 imdistanri 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) )
35 ovif 
 |-  ( if ( k = L , M , ( 0g ` A ) ) .* ( k .^ X ) ) = if ( k = L , ( M .* ( k .^ X ) ) , ( ( 0g ` A ) .* ( k .^ X ) ) )
36 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
37 9 ply1sca 
 |-  ( A e. Ring -> A = ( Scalar ` Q ) )
38 36 37 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A = ( Scalar ` Q ) )
39 38 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> A = ( Scalar ` Q ) )
40 39 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( 0g ` A ) = ( 0g ` ( Scalar ` Q ) ) )
41 40 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( 0g ` A ) .* ( k .^ X ) ) = ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) )
42 9 ply1lmod 
 |-  ( A e. Ring -> Q e. LMod )
43 36 42 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. LMod )
44 43 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> Q e. LMod )
45 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
46 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
47 45 46 mgpbas 
 |-  ( Base ` Q ) = ( Base ` ( mulGrp ` Q ) )
48 9 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
49 36 48 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
50 45 ringmgp 
 |-  ( Q e. Ring -> ( mulGrp ` Q ) e. Mnd )
51 49 50 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( mulGrp ` Q ) e. Mnd )
52 51 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( mulGrp ` Q ) e. Mnd )
53 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> k e. NN0 )
54 6 9 46 vr1cl 
 |-  ( A e. Ring -> X e. ( Base ` Q ) )
55 36 54 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> X e. ( Base ` Q ) )
56 55 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> X e. ( Base ` Q ) )
57 47 5 52 53 56 mulgnn0cld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` Q ) )
58 eqid 
 |-  ( Scalar ` Q ) = ( Scalar ` Q )
59 eqid 
 |-  ( 0g ` ( Scalar ` Q ) ) = ( 0g ` ( Scalar ` Q ) )
60 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
61 46 58 4 59 60 lmod0vs 
 |-  ( ( Q e. LMod /\ ( k .^ X ) e. ( Base ` Q ) ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( 0g ` Q ) )
62 44 57 61 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( 0g ` Q ) )
63 41 62 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( 0g ` A ) .* ( k .^ X ) ) = ( 0g ` Q ) )
64 63 ifeq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> if ( k = L , ( M .* ( k .^ X ) ) , ( ( 0g ` A ) .* ( k .^ X ) ) ) = if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) )
65 35 64 eqtrid 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( if ( k = L , M , ( 0g ` A ) ) .* ( k .^ X ) ) = if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) )
66 34 65 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( if ( k = L , M , ( 0g ` A ) ) .* ( k .^ X ) ) = if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) )
67 30 66 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) = if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) )
68 67 mpteq2dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( k e. NN0 |-> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) ) = ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) ) )
69 68 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( Q gsum ( k e. NN0 |-> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) ) ) = ( Q gsum ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) ) ) )
70 ringmnd 
 |-  ( Q e. Ring -> Q e. Mnd )
71 49 70 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Mnd )
72 71 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> Q e. Mnd )
73 nn0ex 
 |-  NN0 e. _V
74 73 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> NN0 e. _V )
75 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> L e. NN0 )
76 eqid 
 |-  ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) ) = ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) )
77 38 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` A ) = ( Base ` ( Scalar ` Q ) ) )
78 8 77 eqtrid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> K = ( Base ` ( Scalar ` Q ) ) )
79 78 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( M e. K <-> M e. ( Base ` ( Scalar ` Q ) ) ) )
80 79 biimpcd 
 |-  ( M e. K -> ( ( N e. Fin /\ R e. Ring ) -> M e. ( Base ` ( Scalar ` Q ) ) ) )
81 80 adantr 
 |-  ( ( M e. K /\ L e. NN0 ) -> ( ( N e. Fin /\ R e. Ring ) -> M e. ( Base ` ( Scalar ` Q ) ) ) )
82 81 impcom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> M e. ( Base ` ( Scalar ` Q ) ) )
83 82 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> M e. ( Base ` ( Scalar ` Q ) ) )
84 eqid 
 |-  ( Base ` ( Scalar ` Q ) ) = ( Base ` ( Scalar ` Q ) )
85 46 58 4 84 lmodvscl 
 |-  ( ( Q e. LMod /\ M e. ( Base ` ( Scalar ` Q ) ) /\ ( k .^ X ) e. ( Base ` Q ) ) -> ( M .* ( k .^ X ) ) e. ( Base ` Q ) )
86 44 83 57 85 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( M .* ( k .^ X ) ) e. ( Base ` Q ) )
87 86 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> A. k e. NN0 ( M .* ( k .^ X ) ) e. ( Base ` Q ) )
88 60 72 74 75 76 87 gsummpt1n0 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> ( Q gsum ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) ) ) = [_ L / k ]_ ( M .* ( k .^ X ) ) )
89 15 88 sylanl2 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( Q gsum ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) ) ) = [_ L / k ]_ ( M .* ( k .^ X ) ) )
90 69 89 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( Q gsum ( k e. NN0 |-> ( ( ( ( L E Y ) .x. ( T ` M ) ) decompPMat k ) .* ( k .^ X ) ) ) ) = [_ L / k ]_ ( M .* ( k .^ X ) ) )
91 csbov2g 
 |-  ( L e. NN0 -> [_ L / k ]_ ( M .* ( k .^ X ) ) = ( M .* [_ L / k ]_ ( k .^ X ) ) )
92 csbov1g 
 |-  ( L e. NN0 -> [_ L / k ]_ ( k .^ X ) = ( [_ L / k ]_ k .^ X ) )
93 csbvarg 
 |-  ( L e. NN0 -> [_ L / k ]_ k = L )
94 93 oveq1d 
 |-  ( L e. NN0 -> ( [_ L / k ]_ k .^ X ) = ( L .^ X ) )
95 92 94 eqtrd 
 |-  ( L e. NN0 -> [_ L / k ]_ ( k .^ X ) = ( L .^ X ) )
96 95 oveq2d 
 |-  ( L e. NN0 -> ( M .* [_ L / k ]_ ( k .^ X ) ) = ( M .* ( L .^ X ) ) )
97 91 96 eqtrd 
 |-  ( L e. NN0 -> [_ L / k ]_ ( M .* ( k .^ X ) ) = ( M .* ( L .^ X ) ) )
98 97 ad2antll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> [_ L / k ]_ ( M .* ( k .^ X ) ) = ( M .* ( L .^ X ) ) )
99 21 90 98 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( I ` ( ( L E Y ) .x. ( T ` M ) ) ) = ( M .* ( L .^ X ) ) )