Definition df-mat 20420

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 = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ((𝑟 freeLMod (𝑛 × 𝑛)) sSet ⟨(.r‘ndx), (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)⟩))

Distinct variable group:   𝑛,𝑟

Detailed syntax breakdown of Definition df-mat

Step	Hyp	Ref	Expression
1		cmat 20419	. 2 class Mat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8189	. . 3 class Fin
5		cvv 3390	. . 3 class V
6	3	cv 1636	. . . . 5 class 𝑟
7	2	cv 1636	. . . . . 6 class 𝑛
8	7, 7	cxp 5306	. . . . 5 class (𝑛 × 𝑛)
9		cfrlm 20296	. . . . 5 class freeLMod
10	6, 8, 9	co 6871	. . . 4 class (𝑟 freeLMod (𝑛 × 𝑛))
11		cnx 16061	. . . . . 6 class ndx
12		cmulr 16150	. . . . . 6 class .r
13	11, 12	cfv 6098	. . . . 5 class (.r‘ndx)
14	7, 7, 7	cotp 4375	. . . . . 6 class ⟨𝑛, 𝑛, 𝑛⟩
15		cmmul 20395	. . . . . 6 class maMul
16	6, 14, 15	co 6871	. . . . 5 class (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)
17	13, 16	cop 4373	. . . 4 class ⟨(.r‘ndx), (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)⟩
18		csts 16062	. . . 4 class sSet
19	10, 17, 18	co 6871	. . 3 class ((𝑟 freeLMod (𝑛 × 𝑛)) sSet ⟨(.r‘ndx), (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)⟩)
20	2, 3, 4, 5, 19	cmpt2 6873	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ((𝑟 freeLMod (𝑛 × 𝑛)) sSet ⟨(.r‘ndx), (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)⟩))
21	1, 20	wceq 1637	1 wff Mat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ((𝑟 freeLMod (𝑛 × 𝑛)) sSet ⟨(.r‘ndx), (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)⟩))

This definition is referenced by:  matbas0pc  20421  matbas0  20422  matval  20423  matrcl  20424  mdetfval  20599  madufval  20650