Definition df-mat2pmat 22429

Description: Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019.)

Assertion

Ref	Expression
df-mat2pmat	⊢ matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))

Distinct variable group:   𝑚,𝑛,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-mat2pmat

Step	Hyp	Ref	Expression
1		cmat2pmat 22426	. 2 class matToPolyMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8941	. . 3 class Fin
5		cvv 3472	. . 3 class V
6		vm	. . . 4 setvar 𝑚
7	2	cv 1538	. . . . . 6 class 𝑛
8	3	cv 1538	. . . . . 6 class 𝑟
9		cmat 22127	. . . . . 6 class Mat
10	7, 8, 9	co 7411	. . . . 5 class (𝑛 Mat 𝑟)
11		cbs 17148	. . . . 5 class Base
12	10, 11	cfv 6542	. . . 4 class (Base‘(𝑛 Mat 𝑟))
13		vx	. . . . 5 setvar 𝑥
14		vy	. . . . 5 setvar 𝑦
15	13	cv 1538	. . . . . . 7 class 𝑥
16	14	cv 1538	. . . . . . 7 class 𝑦
17	6	cv 1538	. . . . . . 7 class 𝑚
18	15, 16, 17	co 7411	. . . . . 6 class (𝑥𝑚𝑦)
19		cpl1 21920	. . . . . . . 8 class Poly1
20	8, 19	cfv 6542	. . . . . . 7 class (Poly1‘𝑟)
21		cascl 21626	. . . . . . 7 class algSc
22	20, 21	cfv 6542	. . . . . 6 class (algSc‘(Poly1‘𝑟))
23	18, 22	cfv 6542	. . . . 5 class ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))
24	13, 14, 7, 7, 23	cmpo 7413	. . . 4 class (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))
25	6, 12, 24	cmpt 5230	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))))
26	2, 3, 4, 5, 25	cmpo 7413	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))
27	1, 26	wceq 1539	1 wff matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))

This definition is referenced by:  mat2pmatfval  22445