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 = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))))$

Step	Hyp	Ref	Expression
0		cmat2pmat	$class matToPolyMat$
1		vn	$setvar n$
2		cfn	$class Fin$
3		vr	$setvar r$
4		cvv	$class V$
5		vm	$setvar m$
6		cbs	$class Base$
7	1	cv	$setvar n$
8		cmat	$class Mat$
9	3	cv	$setvar r$
10	7 9 8	co	$class (n Mat r)$
11	10 6	cfv	$class {Base}_{(n Mat r)}$
12		vx	$setvar x$
13		vy	$setvar y$
14		cascl	$class algSc$
15		cpl1	$class {Poly}_{1}$
16	9 15	cfv	$class {Poly}_{1} (r)$
17	16 14	cfv	$class algSc ({Poly}_{1} (r))$
18	12	cv	$setvar x$
19	5	cv	$setvar m$
20	13	cv	$setvar y$
21	18 20 19	co	$class (x m y)$
22	21 17	cfv	$class algSc ({Poly}_{1} (r)) (x m y)$
23	12 13 7 7 22	cmpo	$class (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))$
24	5 11 23	cmpt	$class (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y)))$
25	1 3 2 4 24	cmpo	$class (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))))$
26	0 25	wceq	$wff matToPolyMat = (n \in Fin, r \in V ⟼ (m \in {Base}_{(n Mat r)} ⟼ (x \in n, y \in n ⟼ algSc ({Poly}_{1} (r)) (x m y))))$

Metamath Proof Explorer