Theorem decpmate

Description: An entry of the matrix consisting of the coefficients in the entries of a polynomial matrix is the corresponding coefficient in the polynomial entry of the given matrix. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	decpmate.p	|- P = ( Poly1 ` R )
	decpmate.c	|- C = ( N Mat P )
	decpmate.b	|- B = ( Base ` C )
Assertion	decpmate	|- ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> ( I ( M decompPMat K ) J ) = ( ( coe1 ` ( I M J ) ) ` K ) )

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	2 3	decpmatval	|- ( ( M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
5	4	3adant1	|- ( ( R e. V /\ M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
6	5	adantr	|- ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
7		oveq12	|- ( ( i = I /\ j = J ) -> ( i M j ) = ( I M J ) )
8	7	fveq2d	|- ( ( i = I /\ j = J ) -> ( coe1 ` ( i M j ) ) = ( coe1 ` ( I M J ) ) )
9	8	fveq1d	|- ( ( i = I /\ j = J ) -> ( ( coe1 ` ( i M j ) ) ` K ) = ( ( coe1 ` ( I M J ) ) ` K ) )
10	9	adantl	|- ( ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> ( ( coe1 ` ( i M j ) ) ` K ) = ( ( coe1 ` ( I M J ) ) ` K ) )
11		simprl	|- ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> I e. N )
12		simprr	|- ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> J e. N )
13		fvexd	|- ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> ( ( coe1 ` ( I M J ) ) ` K ) e. _V )
14	6 10 11 12 13	ovmpod	|- ( ( ( R e. V /\ M e. B /\ K e. NN0 ) /\ ( I e. N /\ J e. N ) ) -> ( I ( M decompPMat K ) J ) = ( ( coe1 ` ( I M J ) ) ` K ) )