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 = (n \in Fin, r \in V ⟼ (m \in (n ConstPolyMat r) ⟼ (x \in n, y \in n ⟼ {coe}_{1} (x m y) (0))))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccpmat2mat	$class cPolyMatToMat$
1		vn	$setvar n$
2		cfn	$class Fin$
3		vr	$setvar r$
4		cvv	$class V$
5		vm	$setvar m$
6	1	cv	$setvar n$
7		ccpmat	$class ConstPolyMat$
8	3	cv	$setvar r$
9	6 8 7	co	$class (n ConstPolyMat r)$
10		vx	$setvar x$
11		vy	$setvar y$
12		cco1	$class {coe}_{1}$
13	10	cv	$setvar x$
14	5	cv	$setvar m$
15	11	cv	$setvar y$
16	13 15 14	co	$class (x m y)$
17	16 12	cfv	$class {coe}_{1} (x m y)$
18		cc0	$class 0$
19	18 17	cfv	$class {coe}_{1} (x m y) (0)$
20	10 11 6 6 19	cmpo	$class (x \in n, y \in n ⟼ {coe}_{1} (x m y) (0))$
21	5 9 20	cmpt	$class (m \in (n ConstPolyMat r) ⟼ (x \in n, y \in n ⟼ {coe}_{1} (x m y) (0)))$
22	1 3 2 4 21	cmpo	$class (n \in Fin, r \in V ⟼ (m \in (n ConstPolyMat r) ⟼ (x \in n, y \in n ⟼ {coe}_{1} (x m y) (0))))$
23	0 22	wceq	$wff cPolyMatToMat = (n \in Fin, r \in V ⟼ (m \in (n ConstPolyMat r) ⟼ (x \in n, y \in n ⟼ {coe}_{1} (x m y) (0))))$

Metamath Proof Explorer

Definition df-cpmat2mat

Detailed syntax breakdown