Theorem pm2mpf

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 5-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 )
	pm2mpcl.l	|- L = ( Base ` Q )
Assertion	pm2mpf	|- ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )

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		pm2mpcl.l	|- L = ( Base ` Q )
11		ovexd	|- ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) -> ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) e. _V )
12	1 2 3 4 5 6 7 8 9	pm2mpval	|- ( ( N e. Fin /\ R e. Ring ) -> T = ( m e. B |-> ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) )
13	1 2 3 4 5 6 7 8 9 10	pm2mpcl	|- ( ( N e. Fin /\ R e. Ring /\ b e. B ) -> ( T ` b ) e. L )
14	13	3expa	|- ( ( ( N e. Fin /\ R e. Ring ) /\ b e. B ) -> ( T ` b ) e. L )
15	11 12 14	fmpt2d	|- ( ( N e. Fin /\ R e. Ring ) -> T : B --> L )