Metamath Proof Explorer

Theorem pm2mpfval

Description: A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-Oct-2019) (Revised by AV, 5-Dec-2019)

		Ref	Expression
	Hypotheses	pm2mpval.p	\|- P = ( Poly1 ` R )
		pm2mpval.c	\|- C = ( N Mat P )
		pm2mpval.b	\|- B = ( Base ` C )
		pm2mpval.m	\|- .* = ( .s ` Q )
		pm2mpval.e	\|- .^ = ( .g ` ( mulGrp ` Q ) )
		pm2mpval.x	\|- X = ( var1 ` A )
		pm2mpval.a	\|- A = ( N Mat R )
		pm2mpval.q	\|- Q = ( Poly1 ` A )
		pm2mpval.t	\|- T = ( N pMatToMatPoly R )
	Assertion	pm2mpfval	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( T ` M ) = ( Q gsum ( k e. NN0 \|-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpval.p	\|- P = ( Poly1 ` R )
2		pm2mpval.c	\|- C = ( N Mat P )
3		pm2mpval.b	\|- B = ( Base ` C )
4		pm2mpval.m	\|- .* = ( .s ` Q )
5		pm2mpval.e	\|- .^ = ( .g ` ( mulGrp ` Q ) )
6		pm2mpval.x	\|- X = ( var1 ` A )
7		pm2mpval.a	\|- A = ( N Mat R )
8		pm2mpval.q	\|- Q = ( Poly1 ` A )
9		pm2mpval.t	\|- T = ( N pMatToMatPoly R )
10	1 2 3 4 5 6 7 8 9	pm2mpval	\|- ( ( N e. Fin /\ R e. V ) -> T = ( m e. B \|-> ( Q gsum ( k e. NN0 \|-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) )
11	10	3adant3	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> T = ( m e. B \|-> ( Q gsum ( k e. NN0 \|-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) )
12		oveq1	\|- ( m = M -> ( m decompPMat k ) = ( M decompPMat k ) )
13	12	oveq1d	\|- ( m = M -> ( ( m decompPMat k ) .* ( k .^ X ) ) = ( ( M decompPMat k ) .* ( k .^ X ) ) )
14	13	mpteq2dv	\|- ( m = M -> ( k e. NN0 \|-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) = ( k e. NN0 \|-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) )
15	14	oveq2d	\|- ( m = M -> ( Q gsum ( k e. NN0 \|-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) = ( Q gsum ( k e. NN0 \|-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) )
16	15	adantl	\|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ m = M ) -> ( Q gsum ( k e. NN0 \|-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) = ( Q gsum ( k e. NN0 \|-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) )
17		simp3	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> M e. B )
18		ovexd	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( Q gsum ( k e. NN0 \|-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) e. _V )
19	11 16 17 18	fvmptd	\|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( T ` M ) = ( Q gsum ( k e. NN0 \|-> ( ( M decompPMat k ) .* ( k .^ X ) ) ) ) )