Metamath Proof Explorer

Theorem decpmatcl

Description: Closure of the decomposition of a polynomial matrix: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power is a matrix. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

Ref Expression
Hypotheses decpmate.p 
|- P = ( Poly1 ` R )
decpmate.c 
|- C = ( N Mat P )
decpmate.b 
|- B = ( Base ` C )
decpmatcl.a 
|- A = ( N Mat R )
decpmatcl.d 
|- D = ( Base ` A )
Assertion decpmatcl 
|- ( ( R e. V /\ M e. B /\ K e. NN0 ) -> ( M decompPMat K ) e. D )

Proof

Step Hyp Ref Expression
1 decpmate.p 
 |-  P = ( Poly1 ` R )
2 decpmate.c 
 |-  C = ( N Mat P )
3 decpmate.b 
 |-  B = ( Base ` C )
4 decpmatcl.a 
 |-  A = ( N Mat R )
5 decpmatcl.d 
 |-  D = ( Base ` A )
6 2 3 decpmatval 
 |-  ( ( M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
7 6 3adant1 
 |-  ( ( R e. V /\ M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 2 3 matrcl 
 |-  ( M e. B -> ( N e. Fin /\ P e. _V ) )
10 9 simpld 
 |-  ( M e. B -> N e. Fin )
11 10 3ad2ant2 
 |-  ( ( R e. V /\ M e. B /\ K e. NN0 ) -> N e. Fin )
12 simp1 
 |-  ( ( R e. V /\ M e. B /\ K e. NN0 ) -> R e. V )
13 eqid 
 |-  ( Base ` P ) = ( Base ` P )
14 simp2 
 |-  ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> i e. N )
15 simp3 
 |-  ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> j e. N )
16 simp2 
 |-  ( ( R e. V /\ M e. B /\ K e. NN0 ) -> M e. B )
17 16 3ad2ant1 
 |-  ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> M e. B )
18 2 13 3 14 15 17 matecld 
 |-  ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` P ) )
19 simp3 
 |-  ( ( R e. V /\ M e. B /\ K e. NN0 ) -> K e. NN0 )
20 19 3ad2ant1 
 |-  ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> K e. NN0 )
21 eqid 
 |-  ( coe1 ` ( i M j ) ) = ( coe1 ` ( i M j ) )
22 21 13 1 8 coe1fvalcl 
 |-  ( ( ( i M j ) e. ( Base ` P ) /\ K e. NN0 ) -> ( ( coe1 ` ( i M j ) ) ` K ) e. ( Base ` R ) )
23 18 20 22 syl2anc 
 |-  ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ i e. N /\ j e. N ) -> ( ( coe1 ` ( i M j ) ) ` K ) e. ( Base ` R ) )
24 4 8 5 11 12 23 matbas2d 
 |-  ( ( R e. V /\ M e. B /\ K e. NN0 ) -> ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) e. D )
25 7 24 eqeltrd 
 |-  ( ( R e. V /\ M e. B /\ K e. NN0 ) -> ( M decompPMat K ) e. D )