Metamath Proof Explorer

Theorem pmatcollpw2

Description: Write a polynomial matrix as a sum of matrices whose entries are products of variable powers and constant polynomials collecting like powers. (Contributed by AV, 3-Oct-2019) (Revised by AV, 3-Dec-2019)

Ref Expression
Hypotheses pmatcollpw1.p 
|- P = ( Poly1 ` R )
pmatcollpw1.c 
|- C = ( N Mat P )
pmatcollpw1.b 
|- B = ( Base ` C )
pmatcollpw1.m 
|- .X. = ( .s ` P )
pmatcollpw1.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw1.x 
|- X = ( var1 ` R )
Assertion pmatcollpw2 
|- ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( C gsum ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw1.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw1.c 
 |-  C = ( N Mat P )
3 pmatcollpw1.b 
 |-  B = ( Base ` C )
4 pmatcollpw1.m 
 |-  .X. = ( .s ` P )
5 pmatcollpw1.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw1.x 
 |-  X = ( var1 ` R )
7 1 2 3 4 5 6 pmatcollpw1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )
8 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
9 simp1 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> N e. Fin )
10 nn0ex 
 |-  NN0 e. _V
11 10 a1i 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> NN0 e. _V )
12 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
13 12 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> P e. Ring )
14 eqid 
 |-  ( Base ` P ) = ( Base ` P )
15 9 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) -> N e. Fin )
16 13 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) -> P e. Ring )
17 simp1l2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> R e. Ring )
18 eqid 
 |-  ( N Mat R ) = ( N Mat R )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
21 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
22 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
23 simp2 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> R e. Ring )
24 23 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) -> R e. Ring )
25 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M e. B )
26 25 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) -> M e. B )
27 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) -> n e. NN0 )
28 24 26 27 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) -> ( R e. Ring /\ M e. B /\ n e. NN0 ) )
29 28 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( R e. Ring /\ M e. B /\ n e. NN0 ) )
30 1 2 3 18 20 decpmatcl 
 |-  ( ( R e. Ring /\ M e. B /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
31 29 30 syl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
32 18 19 20 21 22 31 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( i ( M decompPMat n ) j ) e. ( Base ` R ) )
33 simp1r 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> n e. NN0 )
34 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
35 19 1 6 4 34 5 14 ply1tmcl 
 |-  ( ( R e. Ring /\ ( i ( M decompPMat n ) j ) e. ( Base ` R ) /\ n e. NN0 ) -> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) e. ( Base ` P ) )
36 17 32 33 35 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) e. ( Base ` P ) )
37 2 14 3 15 16 36 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ n e. NN0 ) -> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) e. B )
38 1 2 3 4 5 6 pmatcollpw2lem 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) finSupp ( 0g ` C ) )
39 2 3 8 9 11 13 37 38 matgsum 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( C gsum ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) = ( i e. N , j e. N |-> ( P gsum ( n e. NN0 |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )
40 7 39 eqtr4d 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> M = ( C gsum ( n e. NN0 |-> ( i e. N , j e. N |-> ( ( i ( M decompPMat n ) j ) .X. ( n .^ X ) ) ) ) ) )