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 >. ) >. ) )