Metamath Proof Explorer

Theorem pm2mpcl

Description: The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019) (Revised by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p 
|- P = ( Poly1 ` R )
pm2mpval.c 
|- C = ( N Mat P )
pm2mpval.b 
|- B = ( Base ` C )
pm2mpval.m 
|- .* = ( .s ` Q )
pm2mpval.e 
|- .^ = ( .g ` ( mulGrp ` Q ) )
pm2mpval.x 
|- X = ( var1 ` A )
pm2mpval.a 
|- A = ( N Mat R )
pm2mpval.q 
|- Q = ( Poly1 ` A )
pm2mpval.t 
|- T = ( N pMatToMatPoly R )
pm2mpcl.l 
|- L = ( Base ` Q )
Assertion pm2mpcl 
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. L )

Proof

Step Hyp Ref Expression
1 pm2mpval.p 
 |-  P = ( Poly1 ` R )
2 pm2mpval.c 
 |-  C = ( N Mat P )
3 pm2mpval.b 
 |-  B = ( Base ` C )
4 pm2mpval.m 
 |-  .* = ( .s ` Q )
5 pm2mpval.e 
 |-  .^ = ( .g ` ( mulGrp ` Q ) )
6 pm2mpval.x 
 |-  X = ( var1 ` A )
7 pm2mpval.a 
 |-  A = ( N Mat R )
8 pm2mpval.q 
 |-  Q = ( Poly1 ` A )
9 pm2mpval.t 
 |-  T = ( N pMatToMatPoly R )
10 pm2mpcl.l 
 |-  L = ( Base ` Q )
11 1 2 3 4 5 6 7 8 9 pm2mpfval 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) = ( Q gsum ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) )
12 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
13 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
14 8 ply1ring 
 |-  ( A e. Ring -> Q e. Ring )
15 ringcmn 
 |-  ( Q e. Ring -> Q e. CMnd )
16 13 14 15 3syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Q e. CMnd )
17 16 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Q e. CMnd )
18 nn0ex 
 |-  NN0 e. _V
19 18 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> NN0 e. _V )
20 13 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> A e. Ring )
21 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> A e. Ring )
22 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> R e. Ring )
23 simpl3 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> M e. B )
24 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> k e. NN0 )
25 eqid 
 |-  ( Base ` A ) = ( Base ` A )
26 1 2 3 7 25 decpmatcl 
 |-  ( ( R e. Ring /\ M e. B /\ k e. NN0 ) -> ( M decompPMat k ) e. ( Base ` A ) )
27 22 23 24 26 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> ( M decompPMat k ) e. ( Base ` A ) )
28 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
29 25 8 6 4 28 5 10 ply1tmcl 
 |-  ( ( A e. Ring /\ ( M decompPMat k ) e. ( Base ` A ) /\ k e. NN0 ) -> ( ( M decompPMat k ) .* ( k .^ X ) ) e. L )
30 21 27 24 29 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> ( ( M decompPMat k ) .* ( k .^ X ) ) e. L )
31 30 fmpttd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) : NN0 --> L )
32 8 ply1lmod 
 |-  ( A e. Ring -> Q e. LMod )
33 20 32 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Q e. LMod )
34 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( Scalar ` Q ) = ( Scalar ` Q ) )
35 8 6 28 5 10 ply1moncl 
 |-  ( ( A e. Ring /\ k e. NN0 ) -> ( k .^ X ) e. L )
36 20 35 sylan 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ k e. NN0 ) -> ( k .^ X ) e. L )
37 eqid 
 |-  ( 0g ` ( Scalar ` Q ) ) = ( 0g ` ( Scalar ` Q ) )
38 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
39 1 2 3 7 38 decpmatfsupp 
 |-  ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp ( 0g ` A ) )
40 39 3adant1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp ( 0g ` A ) )
41 8 ply1sca 
 |-  ( A e. Ring -> A = ( Scalar ` Q ) )
42 41 eqcomd 
 |-  ( A e. Ring -> ( Scalar ` Q ) = A )
43 20 42 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( Scalar ` Q ) = A )
44 43 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( 0g ` ( Scalar ` Q ) ) = ( 0g ` A ) )
45 40 44 breqtrrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp ( 0g ` ( Scalar ` Q ) ) )
46 19 33 34 10 27 36 12 37 4 45 mptscmfsupp0 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) finSupp ( 0g ` Q ) )
47 10 12 17 19 31 46 gsumcl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( Q gsum ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) e. L )
48 11 47 eqeltrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. L )