# 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 ${⊢}\mathrm{Mat}=\left({n}\in \mathrm{Fin},{r}\in \mathrm{V}⟼\left({r}\mathrm{freeLMod}\left({n}×{n}\right)\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{r}\mathrm{maMul}⟨{n},{n},{n}⟩⟩\right)$

### Detailed syntax breakdown

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