Metamath Proof Explorer

Theorem pmatcollpwfi

Description: Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019) (Revised by AV, 4-Dec-2019) (Proof shortened by AV, 3-Jul-2022)

Ref Expression
Hypotheses pmatcollpw.p 
|- P = ( Poly1 ` R )
pmatcollpw.c 
|- C = ( N Mat P )
pmatcollpw.b 
|- B = ( Base ` C )
pmatcollpw.m 
|- .* = ( .s ` C )
pmatcollpw.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw.x 
|- X = ( var1 ` R )
pmatcollpw.t 
|- T = ( N matToPolyMat R )
Assertion pmatcollpwfi 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw.c 
 |-  C = ( N Mat P )
3 pmatcollpw.b 
 |-  B = ( Base ` C )
4 pmatcollpw.m 
 |-  .* = ( .s ` C )
5 pmatcollpw.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw.x 
 |-  X = ( var1 ` R )
7 pmatcollpw.t 
 |-  T = ( N matToPolyMat R )
8 crngring 
 |-  ( R e. CRing -> R e. Ring )
9 8 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
10 simp3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> M e. B )
11 eqid 
 |-  ( N Mat R ) = ( N Mat R )
12 eqid 
 |-  ( 0g ` ( N Mat R ) ) = ( 0g ` ( N Mat R ) )
13 1 2 3 11 12 decpmataa0 
 |-  ( ( R e. Ring /\ M e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) )
14 9 10 13 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) )
15 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 ) ) ) ) ) )
16 15 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) ) -> M = ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
17 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
18 simp1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> N e. Fin )
19 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
20 18 9 19 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> C e. Ring )
21 ringcmn 
 |-  ( C e. Ring -> C e. CMnd )
22 20 21 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> C e. CMnd )
23 22 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) ) -> C e. CMnd )
24 18 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> N e. Fin )
25 9 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. Ring )
26 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
27 25 26 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> P e. Ring )
28 9 anim1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( R e. Ring /\ n e. NN0 ) )
29 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
30 eqid 
 |-  ( Base ` P ) = ( Base ` P )
31 1 6 29 5 30 ply1moncl 
 |-  ( ( R e. Ring /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
32 28 31 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
33 simpl2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> R e. CRing )
34 10 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> M e. B )
35 simpr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> n e. NN0 )
36 eqid 
 |-  ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
37 1 2 3 11 36 decpmatcl 
 |-  ( ( R e. CRing /\ M e. B /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
38 33 34 35 37 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) )
39 7 11 36 1 2 3 mat2pmatbas0 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( M decompPMat n ) e. ( Base ` ( N Mat R ) ) ) -> ( T ` ( M decompPMat n ) ) e. B )
40 24 25 38 39 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( T ` ( M decompPMat n ) ) e. B )
41 30 2 3 4 matvscl 
 |-  ( ( ( N e. Fin /\ P e. Ring ) /\ ( ( n .^ X ) e. ( Base ` P ) /\ ( T ` ( M decompPMat n ) ) e. B ) ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) e. B )
42 24 27 32 40 41 syl22anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) e. B )
43 42 ralrimiva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> A. n e. NN0 ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) e. B )
44 43 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) ) -> A. n e. NN0 ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) e. B )
45 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) ) -> s e. NN0 )
46 fveq2 
 |-  ( ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) -> ( T ` ( M decompPMat n ) ) = ( T ` ( 0g ` ( N Mat R ) ) ) )
47 9 18 jca 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( R e. Ring /\ N e. Fin ) )
48 47 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( R e. Ring /\ N e. Fin ) )
49 eqid 
 |-  ( 0g ` ( N Mat P ) ) = ( 0g ` ( N Mat P ) )
50 7 1 12 49 0mat2pmat 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( T ` ( 0g ` ( N Mat R ) ) ) = ( 0g ` ( N Mat P ) ) )
51 48 50 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( T ` ( 0g ` ( N Mat R ) ) ) = ( 0g ` ( N Mat P ) ) )
52 46 51 sylan9eqr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) /\ ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> ( T ` ( M decompPMat n ) ) = ( 0g ` ( N Mat P ) ) )
53 52 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) /\ ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) = ( ( n .^ X ) .* ( 0g ` ( N Mat P ) ) ) )
54 1 2 pmatlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. LMod )
55 18 9 54 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> C e. LMod )
56 55 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> C e. LMod )
57 28 adantlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( R e. Ring /\ n e. NN0 ) )
58 57 31 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
59 1 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
60 59 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
61 60 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
62 2 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` C ) )
63 61 62 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` C ) )
64 63 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` C ) = P )
65 64 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( Scalar ` C ) = P )
66 65 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( Base ` ( Scalar ` C ) ) = ( Base ` P ) )
67 58 66 eleqtrrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` ( Scalar ` C ) ) )
68 2 eqcomi 
 |-  ( N Mat P ) = C
69 68 fveq2i 
 |-  ( 0g ` ( N Mat P ) ) = ( 0g ` C )
70 69 oveq2i 
 |-  ( ( n .^ X ) .* ( 0g ` ( N Mat P ) ) ) = ( ( n .^ X ) .* ( 0g ` C ) )
71 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
72 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
73 71 4 72 17 lmodvs0 
 |-  ( ( C e. LMod /\ ( n .^ X ) e. ( Base ` ( Scalar ` C ) ) ) -> ( ( n .^ X ) .* ( 0g ` C ) ) = ( 0g ` C ) )
74 70 73 syl5eq 
 |-  ( ( C e. LMod /\ ( n .^ X ) e. ( Base ` ( Scalar ` C ) ) ) -> ( ( n .^ X ) .* ( 0g ` ( N Mat P ) ) ) = ( 0g ` C ) )
75 56 67 74 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( n .^ X ) .* ( 0g ` ( N Mat P ) ) ) = ( 0g ` C ) )
76 75 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) /\ ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> ( ( n .^ X ) .* ( 0g ` ( N Mat P ) ) ) = ( 0g ` C ) )
77 53 76 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) /\ ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) = ( 0g ` C ) )
78 77 ex 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) = ( 0g ` C ) ) )
79 78 imim2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ n e. NN0 ) -> ( ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> ( s < n -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) = ( 0g ` C ) ) ) )
80 79 ralimdva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) -> ( A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> A. n e. NN0 ( s < n -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) = ( 0g ` C ) ) ) )
81 80 imp 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) ) -> A. n e. NN0 ( s < n -> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) = ( 0g ` C ) ) )
82 3 17 23 44 45 81 gsummptnn0fz 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) ) -> ( C gsum ( n e. NN0 |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
83 16 82 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) /\ A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) ) -> M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )
84 83 ex 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN0 ) -> ( A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) ) )
85 84 reximdva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN0 A. n e. NN0 ( s < n -> ( M decompPMat n ) = ( 0g ` ( N Mat R ) ) ) -> E. s e. NN0 M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) ) )
86 14 85 mpd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 M = ( C gsum ( n e. ( 0 ... s ) |-> ( ( n .^ X ) .* ( T ` ( M decompPMat n ) ) ) ) ) )