Definition df-mat2pmat 22138

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 22135	. 2 class matToPolyMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8922	. . 3 class Fin
5		cvv 3473	. . 3 class V
6		vm	. . . 4 setvar 𝑚
7	2	cv 1540	. . . . . 6 class 𝑛
8	3	cv 1540	. . . . . 6 class 𝑟
9		cmat 21836	. . . . . 6 class Mat
10	7, 8, 9	co 7393	. . . . 5 class (𝑛 Mat 𝑟)
11		cbs 17126	. . . . 5 class Base
12	10, 11	cfv 6532	. . . 4 class (Base‘(𝑛 Mat 𝑟))
13		vx	. . . . 5 setvar 𝑥
14		vy	. . . . 5 setvar 𝑦
15	13	cv 1540	. . . . . . 7 class 𝑥
16	14	cv 1540	. . . . . . 7 class 𝑦
17	6	cv 1540	. . . . . . 7 class 𝑚
18	15, 16, 17	co 7393	. . . . . 6 class (𝑥𝑚𝑦)
19		cpl1 21630	. . . . . . . 8 class Poly1
20	8, 19	cfv 6532	. . . . . . 7 class (Poly1‘𝑟)
21		cascl 21340	. . . . . . 7 class algSc
22	20, 21	cfv 6532	. . . . . 6 class (algSc‘(Poly1‘𝑟))
23	18, 22	cfv 6532	. . . . 5 class ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))
24	13, 14, 7, 7, 23	cmpo 7395	. . . 4 class (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))
25	6, 12, 24	cmpt 5224	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))))
26	2, 3, 4, 5, 25	cmpo 7395	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))
27	1, 26	wceq 1541	1 wff matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))

This definition is referenced by:  mat2pmatfval  22154