# 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 )`