Metamath Proof Explorer

Definition 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 e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmat 
 |-  Mat
1 vn 
 |-  n
2 cfn 
 |-  Fin
3 vr 
 |-  r
4 cvv 
 |-  _V
5 3 cv 
 |-  r
6 cfrlm 
 |-  freeLMod
7 1 cv 
 |-  n
8 7 7 cxp 
 |-  ( n X. n )
9 5 8 6 co 
 |-  ( r freeLMod ( n X. n ) )
10 csts 
 |-  sSet
11 cmulr 
 |-  .r
12 cnx 
 |-  ndx
13 12 11 cfv 
 |-  ( .r ` ndx )
14 cmmul 
 |-  maMul
15 7 7 7 cotp 
 |-  <. n , n , n >.
16 5 15 14 co 
 |-  ( r maMul <. n , n , n >. )
17 13 16 cop 
 |-  <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >.
18 9 17 10 co 
 |-  ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. )
19 1 3 2 4 18 cmpo 
 |-  ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )
20 0 19 wceq 
 |-  Mat = ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )