Definition df-pm2mp 22142

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 = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))))

Distinct variable group:   𝑘,𝑎,𝑛,𝑚,𝑞,𝑟

Detailed syntax breakdown of Definition df-pm2mp

Step	Hyp	Ref	Expression
1		cpm2mp 22141	. 2 class pMatToMatPoly
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8883	. . 3 class Fin
5		cvv 3445	. . 3 class V
6		vm	. . . 4 setvar 𝑚
7	2	cv 1540	. . . . . 6 class 𝑛
8	3	cv 1540	. . . . . . 7 class 𝑟
9		cpl1 21548	. . . . . . 7 class Poly1
10	8, 9	cfv 6496	. . . . . 6 class (Poly1‘𝑟)
11		cmat 21754	. . . . . 6 class Mat
12	7, 10, 11	co 7357	. . . . 5 class (𝑛 Mat (Poly1‘𝑟))
13		cbs 17083	. . . . 5 class Base
14	12, 13	cfv 6496	. . . 4 class (Base‘(𝑛 Mat (Poly1‘𝑟)))
15		va	. . . . 5 setvar 𝑎
16	7, 8, 11	co 7357	. . . . 5 class (𝑛 Mat 𝑟)
17		vq	. . . . . 6 setvar 𝑞
18	15	cv 1540	. . . . . . 7 class 𝑎
19	18, 9	cfv 6496	. . . . . 6 class (Poly1‘𝑎)
20	17	cv 1540	. . . . . . 7 class 𝑞
21		vk	. . . . . . . 8 setvar 𝑘
22		cn0 12413	. . . . . . . 8 class ℕ0
23	6	cv 1540	. . . . . . . . . 10 class 𝑚
24	21	cv 1540	. . . . . . . . . 10 class 𝑘
25		cdecpmat 22111	. . . . . . . . . 10 class decompPMat
26	23, 24, 25	co 7357	. . . . . . . . 9 class (𝑚 decompPMat 𝑘)
27		cv1 21547	. . . . . . . . . . 11 class var1
28	18, 27	cfv 6496	. . . . . . . . . 10 class (var1‘𝑎)
29		cmgp 19896	. . . . . . . . . . . 12 class mulGrp
30	20, 29	cfv 6496	. . . . . . . . . . 11 class (mulGrp‘𝑞)
31		cmg 18872	. . . . . . . . . . 11 class .g
32	30, 31	cfv 6496	. . . . . . . . . 10 class (.g‘(mulGrp‘𝑞))
33	24, 28, 32	co 7357	. . . . . . . . 9 class (𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎))
34		cvsca 17137	. . . . . . . . . 10 class ·𝑠
35	20, 34	cfv 6496	. . . . . . . . 9 class ( ·𝑠 ‘𝑞)
36	26, 33, 35	co 7357	. . . . . . . 8 class ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))
37	21, 22, 36	cmpt 5188	. . . . . . 7 class (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎))))
38		cgsu 17322	. . . . . . 7 class Σg
39	20, 37, 38	co 7357	. . . . . 6 class (𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))
40	17, 19, 39	csb 3855	. . . . 5 class ⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))
41	15, 16, 40	csb 3855	. . . 4 class ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))
42	6, 14, 41	cmpt 5188	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎))))))
43	2, 3, 4, 5, 42	cmpo 7359	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))))
44	1, 43	wceq 1541	1 wff pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))))

This definition is referenced by:  pm2mpval  22144