Metamath Proof Explorer

Theorem decpmatfsupp

Description: The mapping to the matrices consisting of the coefficients in the polynomial entries of a given matrix for the same power is finitely supported. (Contributed by AV, 5-Oct-2019) (Revised by AV, 3-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 )
decpmatfsupp.0 
|- .0. = ( 0g ` A )
Assertion decpmatfsupp 
|- ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp .0. )

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 decpmatfsupp.0 
 |-  .0. = ( 0g ` A )
6 5 fvexi 
 |-  .0. e. _V
7 6 a1i 
 |-  ( ( R e. Ring /\ M e. B ) -> .0. e. _V )
8 ovexd 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ k e. NN0 ) -> ( M decompPMat k ) e. _V )
9 oveq2 
 |-  ( k = x -> ( M decompPMat k ) = ( M decompPMat x ) )
10 1 2 3 4 5 decpmataa0 
 |-  ( ( R e. Ring /\ M e. B ) -> E. s e. NN0 A. x e. NN0 ( s < x -> ( M decompPMat x ) = .0. ) )
11 7 8 9 10 mptnn0fsuppd 
 |-  ( ( R e. Ring /\ M e. B ) -> ( k e. NN0 |-> ( M decompPMat k ) ) finSupp .0. )