Metamath Proof Explorer

Theorem pmatcollpwscmat

Description: Write a scalar matrix over polynomials (over a commutative ring) as a sum of the product of variable powers and constant scalar matrices with scalar entries. (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpwscmat.p 
|- P = ( Poly1 ` R )
pmatcollpwscmat.c 
|- C = ( N Mat P )
pmatcollpwscmat.b 
|- B = ( Base ` C )
pmatcollpwscmat.m1 
|- .* = ( .s ` C )
pmatcollpwscmat.e1 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpwscmat.x 
|- X = ( var1 ` R )
pmatcollpwscmat.t 
|- T = ( N matToPolyMat R )
pmatcollpwscmat.a 
|- A = ( N Mat R )
pmatcollpwscmat.d 
|- D = ( Base ` A )
pmatcollpwscmat.u 
|- U = ( algSc ` P )
pmatcollpwscmat.k 
|- K = ( Base ` R )
pmatcollpwscmat.e2 
|- E = ( Base ` P )
pmatcollpwscmat.s 
|- S = ( algSc ` P )
pmatcollpwscmat.1 
|- .1. = ( 1r ` C )
pmatcollpwscmat.m2 
|- M = ( Q .* .1. )
Assertion pmatcollpwscmat 
|- ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> M = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( ( U ` ( ( coe1 ` Q ) ` n ) ) .* .1. ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpwscmat.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpwscmat.c 
 |-  C = ( N Mat P )
3 pmatcollpwscmat.b 
 |-  B = ( Base ` C )
4 pmatcollpwscmat.m1 
 |-  .* = ( .s ` C )
5 pmatcollpwscmat.e1 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpwscmat.x 
 |-  X = ( var1 ` R )
7 pmatcollpwscmat.t 
 |-  T = ( N matToPolyMat R )
8 pmatcollpwscmat.a 
 |-  A = ( N Mat R )
9 pmatcollpwscmat.d 
 |-  D = ( Base ` A )
10 pmatcollpwscmat.u 
 |-  U = ( algSc ` P )
11 pmatcollpwscmat.k 
 |-  K = ( Base ` R )
12 pmatcollpwscmat.e2 
 |-  E = ( Base ` P )
13 pmatcollpwscmat.s 
 |-  S = ( algSc ` P )
14 pmatcollpwscmat.1 
 |-  .1. = ( 1r ` C )
15 pmatcollpwscmat.m2 
 |-  M = ( Q .* .1. )
16 crngring 
 |-  ( R e. CRing -> R e. Ring )
17 1 2 3 12 4 14 1pmatscmul 
 |-  ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> ( Q .* .1. ) e. B )
18 15 17 eqeltrid 
 |-  ( ( N e. Fin /\ R e. Ring /\ Q e. E ) -> M e. B )
19 16 18 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> M e. B )
20 1 2 3 4 5 6 7 pmatcollpw 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
21 19 20 syld3an3 
 |-  ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> M = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
22 16 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
23 22 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> ( N e. Fin /\ R e. Ring ) )
24 simp3 
 |-  ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> Q e. E )
25 24 anim1ci 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ Q e. E ) /\ n e. NN0 ) -> ( n e. NN0 /\ Q e. E ) )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pmatcollpwscmatlem2 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( n e. NN0 /\ Q e. E ) ) -> ( T ` ( M decompPMat n ) ) = ( ( U ` ( ( coe1 ` Q ) ` n ) ) .* .1. ) )
27 23 25 26 syl2an2r 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ Q e. E ) /\ n e. NN0 ) -> ( T ` ( M decompPMat n ) ) = ( ( U ` ( ( coe1 ` Q ) ` n ) ) .* .1. ) )
28 27 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ Q e. E ) /\ n e. NN0 ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) = ( ( n .^ X ) .* ( ( U ` ( ( coe1 ` Q ) ` n ) ) .* .1. ) ) )
29 28 mpteq2dva 
 |-  ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) = ( n e. NN0 |-> ( ( n .^ X ) .* ( ( U ` ( ( coe1 ` Q ) ` n ) ) .* .1. ) ) ) )
30 29 oveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( ( U ` ( ( coe1 ` Q ) ` n ) ) .* .1. ) ) ) ) )
31 21 30 eqtrd 
 |-  ( ( N e. Fin /\ R e. CRing /\ Q e. E ) -> M = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( ( U ` ( ( coe1 ` Q ) ` n ) ) .* .1. ) ) ) ) )