Metamath Proof Explorer


Theorem cpmatpmat

Description: A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses cpmat.s
|- S = ( N ConstPolyMat R )
cpmat.p
|- P = ( Poly1 ` R )
cpmat.c
|- C = ( N Mat P )
cpmat.b
|- B = ( Base ` C )
Assertion cpmatpmat
|- ( ( N e. Fin /\ R e. V /\ M e. S ) -> M e. B )

Proof

Step Hyp Ref Expression
1 cpmat.s
 |-  S = ( N ConstPolyMat R )
2 cpmat.p
 |-  P = ( Poly1 ` R )
3 cpmat.c
 |-  C = ( N Mat P )
4 cpmat.b
 |-  B = ( Base ` C )
5 1 2 3 4 cpmat
 |-  ( ( N e. Fin /\ R e. V ) -> S = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )
6 5 eleq2d
 |-  ( ( N e. Fin /\ R e. V ) -> ( M e. S <-> M e. { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } ) )
7 elrabi
 |-  ( M e. { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } -> M e. B )
8 6 7 syl6bi
 |-  ( ( N e. Fin /\ R e. V ) -> ( M e. S -> M e. B ) )
9 8 3impia
 |-  ( ( N e. Fin /\ R e. V /\ M e. S ) -> M e. B )