Definition df-pm2mp

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

	Ref	Expression
Assertion	df-pm2mp	⊢ pMatToMatPoly = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat ( Poly1 ‘ 𝑟 ) ) ) ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ⦋ ( Poly1 ‘ 𝑎 ) / 𝑞 ⦌ ( 𝑞 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑚 decompPMat 𝑘 ) ( ·𝑠 ‘ 𝑞 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑞 ) ) ( var1 ‘ 𝑎 ) ) ) ) ) ) )

Detailed syntax breakdown

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