Theorem decpmatval

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix for the same power, general version for arbitrary matrices. (Contributed by AV, 28-Sep-2019) (Revised by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	decpmatval.a	|- A = ( N Mat R )
	decpmatval.b	|- B = ( Base ` A )
Assertion	decpmatval	|- ( ( M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )

Proof

Step	Hyp	Ref	Expression
1		decpmatval.a	|- A = ( N Mat R )
2		decpmatval.b	|- B = ( Base ` A )
3		decpmatval0	|- ( ( M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5	1 4 2	matbas2i	|- ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
6		elmapi	|- ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
7		fdm	|- ( M : ( N X. N ) --> ( Base ` R ) -> dom M = ( N X. N ) )
8	7	dmeqd	|- ( M : ( N X. N ) --> ( Base ` R ) -> dom dom M = dom ( N X. N ) )
9		dmxpid	|- dom ( N X. N ) = N
10	8 9	eqtrdi	|- ( M : ( N X. N ) --> ( Base ` R ) -> dom dom M = N )
11	5 6 10	3syl	|- ( M e. B -> dom dom M = N )
12	11	adantr	|- ( ( M e. B /\ K e. NN0 ) -> dom dom M = N )
13		eqidd	|- ( ( M e. B /\ K e. NN0 ) -> ( ( coe1 ` ( i M j ) ) ` K ) = ( ( coe1 ` ( i M j ) ) ` K ) )
14	12 12 13	mpoeq123dv	|- ( ( M e. B /\ K e. NN0 ) -> ( i e. dom dom M , j e. dom dom M |-> ( ( coe1 ` ( i M j ) ) ` K ) ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )
15	3 14	eqtrd	|- ( ( M e. B /\ K e. NN0 ) -> ( M decompPMat K ) = ( i e. N , j e. N |-> ( ( coe1 ` ( i M j ) ) ` K ) ) )