Definition df-mat 20214

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

Assertion

Ref	Expression
df-mat	|- Mat = ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )

Distinct variable group:   n, r

Detailed syntax breakdown of Definition df-mat

Step	Hyp	Ref	Expression
1		cmat 20213	. 2 class Mat
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cfn 7955	. . 3 class Fin
5		cvv 3200	. . 3 class _V
6	3	cv 1482	. . . . 5 class r
7	2	cv 1482	. . . . . 6 class n
8	7, 7	cxp 5112	. . . . 5 class ( n X. n )
9		cfrlm 20090	. . . . 5 class freeLMod
10	6, 8, 9	co 6650	. . . 4 class ( r freeLMod ( n X. n ) )
11		cnx 15854	. . . . . 6 class ndx
12		cmulr 15942	. . . . . 6 class .r
13	11, 12	cfv 5888	. . . . 5 class ( .r ` ndx )
14	7, 7, 7	cotp 4185	. . . . . 6 class <. n , n , n >.
15		cmmul 20189	. . . . . 6 class maMul
16	6, 14, 15	co 6650	. . . . 5 class ( r maMul <. n , n , n >. )
17	13, 16	cop 4183	. . . 4 class <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >.
18		csts 15855	. . . 4 class sSet
19	10, 17, 18	co 6650	. . 3 class ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. )
20	2, 3, 4, 5, 19	cmpt2 6652	. 2 class ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )
21	1, 20	wceq 1483	1 wff Mat = ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )

This definition is referenced by:  matbas0pc  20215  matbas0  20216  matval  20217  matrcl  20218  mdetfval  20392  madufval  20443