Metamath Proof Explorer

Theorem cpmatel

Description: Property of a constant polynomial matrix. (Contributed by AV, 15-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	cpmatel	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )

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	3adant3	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> S = { m e. B \| A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )
7	6	eleq2d	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( 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 ) } ) )
8		oveq	\|- ( m = M -> ( i m j ) = ( i M j ) )
9	8	fveq2d	\|- ( m = M -> ( coe1 ` ( i m j ) ) = ( coe1 ` ( i M j ) ) )
10	9	fveq1d	\|- ( m = M -> ( ( coe1 ` ( i m j ) ) ` k ) = ( ( coe1 ` ( i M j ) ) ` k ) )
11	10	eqeq1d	\|- ( m = M -> ( ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) <-> ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
12	11	ralbidv	\|- ( m = M -> ( A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) <-> A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
13	12	2ralbidv	\|- ( m = M -> ( A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) <-> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
14	13	elrab	\|- ( 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 /\ A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )
15	7 14	bitrdi	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( M e. S <-> ( M e. B /\ A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) ) )
16	15	3anibar	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( M e. S <-> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i M j ) ) ` k ) = ( 0g ` R ) ) )