Metamath Proof Explorer

Theorem pm2mpcoe1

Description: A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-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 )
Assertion pm2mpcoe1 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( ( coe1 ` ( T ` M ) ) ` K ) = ( M decompPMat K ) )

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 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> N e. Fin )
11 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> R e. Ring )
12 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> M e. B )
13 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 ) ) ) ) )
14 10 11 12 13 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( T ` M ) = ( Q gsum ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) )
15 14 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( coe1 ` ( T ` M ) ) = ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) ) )
16 15 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( ( coe1 ` ( T ` M ) ) ` K ) = ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) ) ` K ) )
17 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
18 7 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
19 18 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> A e. Ring )
20 eqid 
 |-  ( Base ` A ) = ( Base ` A )
21 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
22 11 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> R e. Ring )
23 12 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> M e. B )
24 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> k e. NN0 )
25 1 2 3 7 20 decpmatcl 
 |-  ( ( R e. Ring /\ M e. B /\ k e. NN0 ) -> ( M decompPMat k ) e. ( Base ` A ) )
26 22 23 24 25 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) /\ k e. NN0 ) -> ( M decompPMat k ) e. ( Base ` A ) )
27 26 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> A. k e. NN0 ( M decompPMat k ) e. ( Base ` A ) )
28 1 2 3 7 21 decpmatfsupp 
 |-  ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp ( 0g ` A ) )
29 28 ad2ant2lr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp ( 0g ` A ) )
30 simpr 
 |-  ( ( M e. B /\ K e. NN0 ) -> K e. NN0 )
31 30 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> K e. NN0 )
32 8 17 6 5 19 20 4 21 27 29 31 gsummoncoe1 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( ( coe1 ` ( Q gsum ( k e. NN0 |-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) ) ` K ) = [_ K / k ]_ ( M decompPMat k ) )
33 csbov2g 
 |-  ( K e. NN0 -> [_ K / k ]_ ( M decompPMat k ) = ( M decompPMat [_ K / k ]_ k ) )
34 csbvarg 
 |-  ( K e. NN0 -> [_ K / k ]_ k = K )
35 34 oveq2d 
 |-  ( K e. NN0 -> ( M decompPMat [_ K / k ]_ k ) = ( M decompPMat K ) )
36 33 35 eqtrd 
 |-  ( K e. NN0 -> [_ K / k ]_ ( M decompPMat k ) = ( M decompPMat K ) )
37 36 adantl 
 |-  ( ( M e. B /\ K e. NN0 ) -> [_ K / k ]_ ( M decompPMat k ) = ( M decompPMat K ) )
38 37 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> [_ K / k ]_ ( M decompPMat k ) = ( M decompPMat K ) )
39 16 32 38 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( M e. B /\ K e. NN0 ) ) -> ( ( coe1 ` ( T ` M ) ) ` K ) = ( M decompPMat K ) )