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 9 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
46 36 45 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
47 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
48 47 ringmgp 
 |-  ( Q e. Ring -> ( mulGrp ` Q ) e. Mnd )
49 46 48 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( mulGrp ` Q ) e. Mnd )
50 49 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( mulGrp ` Q ) e. Mnd )
51 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> k e. NN0 )
52 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
53 6 9 52 vr1cl 
 |-  ( A e. Ring -> X e. ( Base ` Q ) )
54 36 53 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> X e. ( Base ` Q ) )
55 54 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> X e. ( Base ` Q ) )
56 47 52 mgpbas 
 |-  ( Base ` Q ) = ( Base ` ( mulGrp ` Q ) )
57 56 5 mulgnn0cl 
 |-  ( ( ( mulGrp ` Q ) e. Mnd /\ k e. NN0 /\ X e. ( Base ` Q ) ) -> ( k .^ X ) e. ( Base ` Q ) )
58 50 51 55 57 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( k .^ X ) e. ( Base ` Q ) )
59 eqid 
 |-  ( Scalar ` Q ) = ( Scalar ` Q )
60 eqid 
 |-  ( 0g ` ( Scalar ` Q ) ) = ( 0g ` ( Scalar ` Q ) )
61 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
62 52 59 4 60 61 lmod0vs 
 |-  ( ( Q e. LMod /\ ( k .^ X ) e. ( Base ` Q ) ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( 0g ` Q ) )
63 44 58 62 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( 0g ` ( Scalar ` Q ) ) .* ( k .^ X ) ) = ( 0g ` Q ) )
64 41 63 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( ( 0g ` A ) .* ( k .^ X ) ) = ( 0g ` Q ) )
65 64 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 ) ) )
66 35 65 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 ) ) )
67 34 66 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 ) ) )
68 30 67 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 ) ) )
69 68 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 ) ) ) )
70 69 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 ) ) ) ) )
71 ringmnd 
 |-  ( Q e. Ring -> Q e. Mnd )
72 46 71 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. Mnd )
73 72 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> Q e. Mnd )
74 nn0ex 
 |-  NN0 e. _V
75 74 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> NN0 e. _V )
76 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> L e. NN0 )
77 eqid 
 |-  ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) ) = ( k e. NN0 |-> if ( k = L , ( M .* ( k .^ X ) ) , ( 0g ` Q ) ) )
78 38 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` A ) = ( Base ` ( Scalar ` Q ) ) )
79 8 78 eqtrid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> K = ( Base ` ( Scalar ` Q ) ) )
80 79 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( M e. K <-> M e. ( Base ` ( Scalar ` Q ) ) ) )
81 80 biimpcd 
 |-  ( M e. K -> ( ( N e. Fin /\ R e. Ring ) -> M e. ( Base ` ( Scalar ` Q ) ) ) )
82 81 adantr 
 |-  ( ( M e. K /\ L e. NN0 ) -> ( ( N e. Fin /\ R e. Ring ) -> M e. ( Base ` ( Scalar ` Q ) ) ) )
83 82 impcom 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> M e. ( Base ` ( Scalar ` Q ) ) )
84 83 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> M e. ( Base ` ( Scalar ` Q ) ) )
85 eqid 
 |-  ( Base ` ( Scalar ` Q ) ) = ( Base ` ( Scalar ` Q ) )
86 52 59 4 85 lmodvscl 
 |-  ( ( Q e. LMod /\ M e. ( Base ` ( Scalar ` Q ) ) /\ ( k .^ X ) e. ( Base ` Q ) ) -> ( M .* ( k .^ X ) ) e. ( Base ` Q ) )
87 44 84 58 86 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) /\ k e. NN0 ) -> ( M .* ( k .^ X ) ) e. ( Base ` Q ) )
88 87 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. K /\ L e. NN0 ) ) -> A. k e. NN0 ( M .* ( k .^ X ) ) e. ( Base ` Q ) )
89 61 73 75 76 77 88 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 ) ) )
90 15 89 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 ) ) )
91 70 90 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 ) ) )
92 csbov2g 
 |-  ( L e. NN0 -> [_ L / k ]_ ( M .* ( k .^ X ) ) = ( M .* [_ L / k ]_ ( k .^ X ) ) )
93 csbov1g 
 |-  ( L e. NN0 -> [_ L / k ]_ ( k .^ X ) = ( [_ L / k ]_ k .^ X ) )
94 csbvarg 
 |-  ( L e. NN0 -> [_ L / k ]_ k = L )
95 94 oveq1d 
 |-  ( L e. NN0 -> ( [_ L / k ]_ k .^ X ) = ( L .^ X ) )
96 93 95 eqtrd 
 |-  ( L e. NN0 -> [_ L / k ]_ ( k .^ X ) = ( L .^ X ) )
97 96 oveq2d 
 |-  ( L e. NN0 -> ( M .* [_ L / k ]_ ( k .^ X ) ) = ( M .* ( L .^ X ) ) )
98 92 97 eqtrd 
 |-  ( L e. NN0 -> [_ L / k ]_ ( M .* ( k .^ X ) ) = ( M .* ( L .^ X ) ) )
99 98 ad2antll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> [_ L / k ]_ ( M .* ( k .^ X ) ) = ( M .* ( L .^ X ) ) )
100 21 91 99 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( M e. K /\ L e. NN0 ) ) -> ( I ` ( ( L E Y ) .x. ( T ` M ) ) ) = ( M .* ( L .^ X ) ) )