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

Step	Hyp	Ref	Expression
0		cmat	⊢ Mat
1		vn	⊢ 𝑛
2		cfn	⊢ Fin
3		vr	⊢ 𝑟
4		cvv	⊢ V
5	3	cv	⊢ 𝑟
6		cfrlm	⊢ freeLMod
7	1	cv	⊢ 𝑛
8	7 7	cxp	⊢ ( 𝑛 × 𝑛 )
9	5 8 6	co	⊢ ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) )
10		csts	⊢ sSet
11		cmulr	⊢ ._r
12		cnx	⊢ ndx
13	12 11	cfv	⊢ ( ._r ‘ ndx )
14		cmmul	⊢ maMul
15	7 7 7	cotp	⊢ ⟨ 𝑛 , 𝑛 , 𝑛 ⟩
16	5 15 14	co	⊢ ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ )
17	13 16	cop	⊢ ⟨ ( ._r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩
18	9 17 10	co	⊢ ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet ⟨ ( ._r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ )
19	1 3 2 4 18	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet ⟨ ( ._r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ ) )
20	0 19	wceq	⊢ Mat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ( ( 𝑟 freeLMod ( 𝑛 × 𝑛 ) ) sSet ⟨ ( ._r ‘ ndx ) , ( 𝑟 maMul ⟨ 𝑛 , 𝑛 , 𝑛 ⟩ ) ⟩ ) )

Metamath Proof Explorer