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 )