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 ∈ Fin , r ∈ V ⟼ r freeLMod n × n sSet ⋅ ndx r maMul n n n

Detailed syntax breakdown

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 × n
9 5 8 6 co class r freeLMod n × n
10 csts class sSet
11 cmulr class ⋅ 𝑟
12 cnx class ndx
13 12 11 cfv class ⋅ 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 ⋅ ndx r maMul n n n
18 9 17 10 co class r freeLMod n × n sSet ⋅ ndx r maMul n n n
19 1 3 2 4 18 cmpo class n ∈ Fin , r ∈ V ⟼ r freeLMod n × n sSet ⋅ ndx r maMul n n n
20 0 19 wceq wff Mat = n ∈ Fin , r ∈ V ⟼ r freeLMod n × n sSet ⋅ ndx r maMul n n n