Definition df-cpmat2mat

Description: Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat , see m2cpminv , it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019)

	Ref	Expression
Assertion	df-cpmat2mat	⊢ cPolyMatToMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccpmat2mat	⊢ cPolyMatToMat
1		vn	⊢ 𝑛
2		cfn	⊢ Fin
3		vr	⊢ 𝑟
4		cvv	⊢ V
5		vm	⊢ 𝑚
6	1	cv	⊢ 𝑛
7		ccpmat	⊢ ConstPolyMat
8	3	cv	⊢ 𝑟
9	6 8 7	co	⊢ ( 𝑛 ConstPolyMat 𝑟 )
10		vx	⊢ 𝑥
11		vy	⊢ 𝑦
12		cco1	⊢ coe1
13	10	cv	⊢ 𝑥
14	5	cv	⊢ 𝑚
15	11	cv	⊢ 𝑦
16	13 15 14	co	⊢ ( 𝑥 𝑚 𝑦 )
17	16 12	cfv	⊢ ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) )
18		cc0	⊢ 0
19	18 17	cfv	⊢ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 )
20	10 11 6 6 19	cmpo	⊢ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) )
21	5 9 20	cmpt	⊢ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) )
22	1 3 2 4 21	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )
23	0 22	wceq	⊢ cPolyMatToMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( 𝑛 ConstPolyMat 𝑟 ) ↦ ( 𝑥 ∈ 𝑛 , 𝑦 ∈ 𝑛 ↦ ( ( coe1 ‘ ( 𝑥 𝑚 𝑦 ) ) ‘ 0 ) ) ) )