Theorem pm2mpval

Description: Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed 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	pm2mpval	|- ( ( N e. Fin /\ R e. V ) -> T = ( m e. B |-> ( 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		df-pm2mp	|- pMatToMatPoly = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) ) )
11	10	a1i	|- ( ( N e. Fin /\ R e. V ) -> pMatToMatPoly = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) ) ) )
12		simpl	|- ( ( n = N /\ r = R ) -> n = N )
13		fveq2	|- ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
14	13	adantl	|- ( ( n = N /\ r = R ) -> ( Poly1 ` r ) = ( Poly1 ` R ) )
15	12 14	oveq12d	|- ( ( n = N /\ r = R ) -> ( n Mat ( Poly1 ` r ) ) = ( N Mat ( Poly1 ` R ) ) )
16	15	fveq2d	|- ( ( n = N /\ r = R ) -> ( Base ` ( n Mat ( Poly1 ` r ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
17	1	oveq2i	|- ( N Mat P ) = ( N Mat ( Poly1 ` R ) )
18	2 17	eqtri	|- C = ( N Mat ( Poly1 ` R ) )
19	18	fveq2i	|- ( Base ` C ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
20	3 19	eqtri	|- B = ( Base ` ( N Mat ( Poly1 ` R ) ) )
21	16 20	eqtr4di	|- ( ( n = N /\ r = R ) -> ( Base ` ( n Mat ( Poly1 ` r ) ) ) = B )
22	21	adantl	|- ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> ( Base ` ( n Mat ( Poly1 ` r ) ) ) = B )
23		ovex	|- ( n Mat r ) e. _V
24		fvexd	|- ( a = ( n Mat r ) -> ( Poly1 ` a ) e. _V )
25		simpr	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> q = ( Poly1 ` a ) )
26		fveq2	|- ( a = ( n Mat r ) -> ( Poly1 ` a ) = ( Poly1 ` ( n Mat r ) ) )
27	26	adantr	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( Poly1 ` a ) = ( Poly1 ` ( n Mat r ) ) )
28	25 27	eqtrd	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> q = ( Poly1 ` ( n Mat r ) ) )
29	28	fveq2d	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( .s ` q ) = ( .s ` ( Poly1 ` ( n Mat r ) ) ) )
30		eqidd	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( m decompPMat k ) = ( m decompPMat k ) )
31	28	fveq2d	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( mulGrp ` q ) = ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) )
32	31	fveq2d	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( .g ` ( mulGrp ` q ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) )
33		eqidd	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> k = k )
34		fveq2	|- ( a = ( n Mat r ) -> ( var1 ` a ) = ( var1 ` ( n Mat r ) ) )
35	34	adantr	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( var1 ` a ) = ( var1 ` ( n Mat r ) ) )
36	32 33 35	oveq123d	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) = ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) )
37	29 30 36	oveq123d	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) = ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) )
38	37	mpteq2dv	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) = ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) ) )
39	28 38	oveq12d	|- ( ( a = ( n Mat r ) /\ q = ( Poly1 ` a ) ) -> ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) = ( ( Poly1 ` ( n Mat r ) ) gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) ) ) )
40	24 39	csbied	|- ( a = ( n Mat r ) -> [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) = ( ( Poly1 ` ( n Mat r ) ) gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) ) ) )
41	23 40	csbie	|- [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) = ( ( Poly1 ` ( n Mat r ) ) gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) ) )
42		oveq12	|- ( ( n = N /\ r = R ) -> ( n Mat r ) = ( N Mat R ) )
43	42	fveq2d	|- ( ( n = N /\ r = R ) -> ( Poly1 ` ( n Mat r ) ) = ( Poly1 ` ( N Mat R ) ) )
44	7	fveq2i	|- ( Poly1 ` A ) = ( Poly1 ` ( N Mat R ) )
45	8 44	eqtri	|- Q = ( Poly1 ` ( N Mat R ) )
46	43 45	eqtr4di	|- ( ( n = N /\ r = R ) -> ( Poly1 ` ( n Mat r ) ) = Q )
47	43	fveq2d	|- ( ( n = N /\ r = R ) -> ( .s ` ( Poly1 ` ( n Mat r ) ) ) = ( .s ` ( Poly1 ` ( N Mat R ) ) ) )
48	45	fveq2i	|- ( .s ` Q ) = ( .s ` ( Poly1 ` ( N Mat R ) ) )
49	4 48	eqtri	|- .* = ( .s ` ( Poly1 ` ( N Mat R ) ) )
50	47 49	eqtr4di	|- ( ( n = N /\ r = R ) -> ( .s ` ( Poly1 ` ( n Mat r ) ) ) = .* )
51		eqidd	|- ( ( n = N /\ r = R ) -> ( m decompPMat k ) = ( m decompPMat k ) )
52	43	fveq2d	|- ( ( n = N /\ r = R ) -> ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) = ( mulGrp ` ( Poly1 ` ( N Mat R ) ) ) )
53	52	fveq2d	|- ( ( n = N /\ r = R ) -> ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( N Mat R ) ) ) ) )
54	45	fveq2i	|- ( mulGrp ` Q ) = ( mulGrp ` ( Poly1 ` ( N Mat R ) ) )
55	54	fveq2i	|- ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( N Mat R ) ) ) )
56	5 55	eqtri	|- .^ = ( .g ` ( mulGrp ` ( Poly1 ` ( N Mat R ) ) ) )
57	53 56	eqtr4di	|- ( ( n = N /\ r = R ) -> ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) = .^ )
58		eqidd	|- ( ( n = N /\ r = R ) -> k = k )
59	42	fveq2d	|- ( ( n = N /\ r = R ) -> ( var1 ` ( n Mat r ) ) = ( var1 ` ( N Mat R ) ) )
60	7	fveq2i	|- ( var1 ` A ) = ( var1 ` ( N Mat R ) )
61	6 60	eqtri	|- X = ( var1 ` ( N Mat R ) )
62	59 61	eqtr4di	|- ( ( n = N /\ r = R ) -> ( var1 ` ( n Mat r ) ) = X )
63	57 58 62	oveq123d	|- ( ( n = N /\ r = R ) -> ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) = ( k .^ X ) )
64	50 51 63	oveq123d	|- ( ( n = N /\ r = R ) -> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) = ( ( m decompPMat k ) .* ( k .^ X ) ) )
65	64	mpteq2dv	|- ( ( n = N /\ r = R ) -> ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) ) = ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) )
66	46 65	oveq12d	|- ( ( n = N /\ r = R ) -> ( ( Poly1 ` ( n Mat r ) ) gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) )
67	66	adantl	|- ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> ( ( Poly1 ` ( n Mat r ) ) gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` ( Poly1 ` ( n Mat r ) ) ) ( k ( .g ` ( mulGrp ` ( Poly1 ` ( n Mat r ) ) ) ) ( var1 ` ( n Mat r ) ) ) ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) )
68	41 67	syl5eq	|- ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) = ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) )
69	22 68	mpteq12dv	|- ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> ( m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ ( Poly1 ` a ) / q ]_ ( q gsum ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k ( .g ` ( mulGrp ` q ) ) ( var1 ` a ) ) ) ) ) ) = ( m e. B |-> ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) )
70		simpl	|- ( ( N e. Fin /\ R e. V ) -> N e. Fin )
71		elex	|- ( R e. V -> R e. _V )
72	71	adantl	|- ( ( N e. Fin /\ R e. V ) -> R e. _V )
73	3	fvexi	|- B e. _V
74	73	mptex	|- ( m e. B |-> ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) e. _V
75	74	a1i	|- ( ( N e. Fin /\ R e. V ) -> ( m e. B |-> ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) e. _V )
76	11 69 70 72 75	ovmpod	|- ( ( N e. Fin /\ R e. V ) -> ( N pMatToMatPoly R ) = ( m e. B |-> ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) )
77	9 76	syl5eq	|- ( ( N e. Fin /\ R e. V ) -> T = ( m e. B |-> ( Q gsum ( k e. NN0 |-> ( ( m decompPMat k ) .* ( k .^ X ) ) ) ) ) )