Definition df-mat2pmat

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmat2pmat	⊢ matToPolyMat
1		vn	⊢ 𝑛
2		cfn	⊢ Fin
3		vr	⊢ 𝑟
4		cvv	⊢ V
5		vm	⊢ 𝑚
6		cbs	⊢ Base
7	1	cv	⊢ 𝑛
8		cmat	⊢ Mat
9	3	cv	⊢ 𝑟
10	7 9 8	co	⊢ ( 𝑛 Mat 𝑟 )
11	10 6	cfv	⊢ ( Base ‘ ( 𝑛 Mat 𝑟 ) )
12		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14		cascl	⊢ algSc
15		cpl1	⊢ Poly1
16	9 15	cfv	⊢ ( Poly1 ‘ 𝑟 )
17	16 14	cfv	⊢ ( algSc ‘ ( Poly1 ‘ 𝑟 ) )
18	12	cv	⊢ 𝑥
19	5	cv	⊢ 𝑚
20	13	cv	⊢ 𝑦
21	18 20 19	co	⊢ ( 𝑥 𝑚 𝑦 )
22	21 17	cfv	⊢ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) )
23	12 13 7 7 22	cmpo	⊢ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) )
24	5 11 23	cmpt	⊢ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) )
25	1 3 2 4 24	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )
26	0 25	wceq	⊢ matToPolyMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( algSc ‘ ( Poly1 ‘ 𝑟 ) ) ‘ ( 𝑥 𝑚 𝑦 ) ) ) ) )