Theorem mply1topmatval

Description: A polynomial over matrices transformed into a polynomial matrix. I is the inverse function of the transformation T of polynomial matrices into polynomials over matrices: ( T( IO ) ) = O ) (see mp2pm2mp ). (Contributed by AV, 6-Oct-2019)

	Ref	Expression
Hypotheses	mply1topmat.a	|- A = ( N Mat R )
	mply1topmat.q	|- Q = ( Poly1 ` A )
	mply1topmat.l	|- L = ( Base ` Q )
	mply1topmat.p	|- P = ( Poly1 ` R )
	mply1topmat.m	|- .x. = ( .s ` P )
	mply1topmat.e	|- E = ( .g ` ( mulGrp ` P ) )
	mply1topmat.y	|- Y = ( var1 ` R )
	mply1topmat.i	|- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
Assertion	mply1topmatval	|- ( ( N e. V /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mply1topmat.a	|- A = ( N Mat R )
2		mply1topmat.q	|- Q = ( Poly1 ` A )
3		mply1topmat.l	|- L = ( Base ` Q )
4		mply1topmat.p	|- P = ( Poly1 ` R )
5		mply1topmat.m	|- .x. = ( .s ` P )
6		mply1topmat.e	|- E = ( .g ` ( mulGrp ` P ) )
7		mply1topmat.y	|- Y = ( var1 ` R )
8		mply1topmat.i	|- I = ( p e. L |-> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
9		fveq2	|- ( p = O -> ( coe1 ` p ) = ( coe1 ` O ) )
10	9	fveq1d	|- ( p = O -> ( ( coe1 ` p ) ` k ) = ( ( coe1 ` O ) ` k ) )
11	10	oveqd	|- ( p = O -> ( i ( ( coe1 ` p ) ` k ) j ) = ( i ( ( coe1 ` O ) ` k ) j ) )
12	11	oveq1d	|- ( p = O -> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) = ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) )
13	12	mpteq2dv	|- ( p = O -> ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) = ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) )
14	13	oveq2d	|- ( p = O -> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) = ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) )
15	14	mpoeq3dv	|- ( p = O -> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` p ) ` k ) j ) .x. ( k E Y ) ) ) ) ) = ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )
16		simpr	|- ( ( N e. V /\ O e. L ) -> O e. L )
17		simpl	|- ( ( N e. V /\ O e. L ) -> N e. V )
18		mpoexga	|- ( ( N e. V /\ N e. V ) -> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. _V )
19	17 18	syldan	|- ( ( N e. V /\ O e. L ) -> ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) e. _V )
20	8 15 16 19	fvmptd3	|- ( ( N e. V /\ O e. L ) -> ( I ` O ) = ( i e. N , j e. N |-> ( P gsum ( k e. NN0 |-> ( ( i ( ( coe1 ` O ) ` k ) j ) .x. ( k E Y ) ) ) ) ) )