Definition df-pm2mp 22747

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 22746	. 2 class pMatToMatPoly
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8967	. . 3 class Fin
5		cvv 3463	. . 3 class V
6		vm	. . . 4 setvar 𝑚
7	2	cv 1538	. . . . . 6 class 𝑛
8	3	cv 1538	. . . . . . 7 class 𝑟
9		cpl1 22126	. . . . . . 7 class Poly1
10	8, 9	cfv 6541	. . . . . 6 class (Poly1‘𝑟)
11		cmat 22359	. . . . . 6 class Mat
12	7, 10, 11	co 7413	. . . . 5 class (𝑛 Mat (Poly1‘𝑟))
13		cbs 17229	. . . . 5 class Base
14	12, 13	cfv 6541	. . . 4 class (Base‘(𝑛 Mat (Poly1‘𝑟)))
15		va	. . . . 5 setvar 𝑎
16	7, 8, 11	co 7413	. . . . 5 class (𝑛 Mat 𝑟)
17		vq	. . . . . 6 setvar 𝑞
18	15	cv 1538	. . . . . . 7 class 𝑎
19	18, 9	cfv 6541	. . . . . 6 class (Poly1‘𝑎)
20	17	cv 1538	. . . . . . 7 class 𝑞
21		vk	. . . . . . . 8 setvar 𝑘
22		cn0 12509	. . . . . . . 8 class ℕ0
23	6	cv 1538	. . . . . . . . . 10 class 𝑚
24	21	cv 1538	. . . . . . . . . 10 class 𝑘
25		cdecpmat 22716	. . . . . . . . . 10 class decompPMat
26	23, 24, 25	co 7413	. . . . . . . . 9 class (𝑚 decompPMat 𝑘)
27		cv1 22125	. . . . . . . . . . 11 class var1
28	18, 27	cfv 6541	. . . . . . . . . 10 class (var1‘𝑎)
29		cmgp 20105	. . . . . . . . . . . 12 class mulGrp
30	20, 29	cfv 6541	. . . . . . . . . . 11 class (mulGrp‘𝑞)
31		cmg 19054	. . . . . . . . . . 11 class .g
32	30, 31	cfv 6541	. . . . . . . . . 10 class (.g‘(mulGrp‘𝑞))
33	24, 28, 32	co 7413	. . . . . . . . 9 class (𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎))
34		cvsca 17277	. . . . . . . . . 10 class ·𝑠
35	20, 34	cfv 6541	. . . . . . . . 9 class ( ·𝑠 ‘𝑞)
36	26, 33, 35	co 7413	. . . . . . . 8 class ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))
37	21, 22, 36	cmpt 5205	. . . . . . 7 class (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎))))
38		cgsu 17456	. . . . . . 7 class Σg
39	20, 37, 38	co 7413	. . . . . 6 class (𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))
40	17, 19, 39	csb 3879	. . . . 5 class ⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))
41	15, 16, 40	csb 3879	. . . 4 class ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))
42	6, 14, 41	cmpt 5205	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎))))))
43	2, 3, 4, 5, 42	cmpo 7415	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))))
44	1, 43	wceq 1539	1 wff pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎)))))))

This definition is referenced by:  pm2mpval  22749