Definition df-pm2mp 20598

Description: Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019.)

Assertion

Ref	Expression
df-pm2mp	|- pMatToMatPoly = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ (Poly1 ` a ) / q ]_ ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) ) ) )

Distinct variable group:   k, a, n, m, q, r

Detailed syntax breakdown of Definition df-pm2mp

Step	Hyp	Ref	Expression
1		cpm2mp 20597	. 2 class pMatToMatPoly
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cfn 7955	. . 3 class Fin
5		cvv 3200	. . 3 class _V
6		vm	. . . 4 setvar m
7	2	cv 1482	. . . . . 6 class n
8	3	cv 1482	. . . . . . 7 class r
9		cpl1 19547	. . . . . . 7 class Poly1
10	8, 9	cfv 5888	. . . . . 6 class (Poly1 ` r )
11		cmat 20213	. . . . . 6 class Mat
12	7, 10, 11	co 6650	. . . . 5 class ( n Mat (Poly1 ` r ) )
13		cbs 15857	. . . . 5 class Base
14	12, 13	cfv 5888	. . . 4 class ( Base ` ( n Mat (Poly1 ` r ) ) )
15		va	. . . . 5 setvar a
16	7, 8, 11	co 6650	. . . . 5 class ( n Mat r )
17		vq	. . . . . 6 setvar q
18	15	cv 1482	. . . . . . 7 class a
19	18, 9	cfv 5888	. . . . . 6 class (Poly1 ` a )
20	17	cv 1482	. . . . . . 7 class q
21		vk	. . . . . . . 8 setvar k
22		cn0 11292	. . . . . . . 8 class NN0
23	6	cv 1482	. . . . . . . . . 10 class m
24	21	cv 1482	. . . . . . . . . 10 class k
25		cdecpmat 20567	. . . . . . . . . 10 class decompPMat
26	23, 24, 25	co 6650	. . . . . . . . 9 class ( m decompPMat k )
27		cv1 19546	. . . . . . . . . . 11 class var1
28	18, 27	cfv 5888	. . . . . . . . . 10 class (var1 ` a )
29		cmgp 18489	. . . . . . . . . . . 12 class mulGrp
30	20, 29	cfv 5888	. . . . . . . . . . 11 class (mulGrp ` q )
31		cmg 17540	. . . . . . . . . . 11 class .g
32	30, 31	cfv 5888	. . . . . . . . . 10 class (.g ` (mulGrp ` q ) )
33	24, 28, 32	co 6650	. . . . . . . . 9 class ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) )
34		cvsca 15945	. . . . . . . . . 10 class .s
35	20, 34	cfv 5888	. . . . . . . . 9 class ( .s ` q )
36	26, 33, 35	co 6650	. . . . . . . 8 class ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) )
37	21, 22, 36	cmpt 4729	. . . . . . 7 class ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) )
38		cgsu 16101	. . . . . . 7 class gsumg
39	20, 37, 38	co 6650	. . . . . 6 class ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) )
40	17, 19, 39	csb 3533	. . . . 5 class [_ (Poly1 ` a ) / q ]_ ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) )
41	15, 16, 40	csb 3533	. . . 4 class [_ ( n Mat r ) / a ]_ [_ (Poly1 ` a ) / q ]_ ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) )
42	6, 14, 41	cmpt 4729	. . 3 class ( m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ (Poly1 ` a ) / q ]_ ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) ) )
43	2, 3, 4, 5, 42	cmpt2 6652	. 2 class ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ (Poly1 ` a ) / q ]_ ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) ) ) )
44	1, 43	wceq 1483	1 wff pMatToMatPoly = ( n e. Fin , r e. _V |-> ( m e. ( Base ` ( n Mat (Poly1 ` r ) ) ) |-> [_ ( n Mat r ) / a ]_ [_ (Poly1 ` a ) / q ]_ ( q gsumg ( k e. NN0 |-> ( ( m decompPMat k ) ( .s ` q ) ( k (.g ` (mulGrp ` q ) ) (var1 ` a ) ) ) ) ) ) )

This definition is referenced by:  pm2mpval  20600