df-mat

Description: Define the algebra of n x n matrices over a ring r. (Contributed by Stefan O'Rear, 31-Aug-2015)

		Ref	Expression
	Assertion	df-mat	$⊢ Mat = (n \in Fin, r \in V ⟼ (r freeLMod (n \times n)) sSet ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩)$

Step	Hyp	Ref	Expression
0		cmat	$class Mat$
1		vn	$setvar n$
2		cfn	$class Fin$
3		vr	$setvar r$
4		cvv	$class V$
5	3	cv	$setvar r$
6		cfrlm	$class freeLMod$
7	1	cv	$setvar n$
8	7 7	cxp	$class (n \times n)$
9	5 8 6	co	$class (r freeLMod (n \times n))$
10		csts	$class sSet$
11		cmulr	$class \cdot_{𝑟}$
12		cnx	$class ndx$
13	12 11	cfv	$class \cdot_{ndx}$
14		cmmul	$class maMul$
15	7 7 7	cotp	$class ⟨n, n, n⟩$
16	5 15 14	co	$class (r maMul ⟨n, n, n⟩)$
17	13 16	cop	$class ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩$
18	9 17 10	co	$class ((r freeLMod (n \times n)) sSet ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩)$
19	1 3 2 4 18	cmpo	$class (n \in Fin, r \in V ⟼ (r freeLMod (n \times n)) sSet ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩)$
20	0 19	wceq	$wff Mat = (n \in Fin, r \in V ⟼ (r freeLMod (n \times n)) sSet ⟨\cdot_{ndx}, r maMul ⟨n, n, n⟩⟩)$

Metamath Proof Explorer