Definition df-dmat

Description: Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in Roman p. 4 or Definition 3.12 in Hefferon p. 240. (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Assertion	df-dmat	⊢ DMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmat	⊢ DMat
1		vn	⊢ 𝑛
2		cfn	⊢ Fin
3		vr	⊢ 𝑟
4		cvv	⊢ V
5		vm	⊢ 𝑚
6		cbs	⊢ Base
7	1	cv	⊢ 𝑛
8		cmat	⊢ Mat
9	3	cv	⊢ 𝑟
10	7 9 8	co	⊢ ( 𝑛 Mat 𝑟 )
11	10 6	cfv	⊢ ( Base ‘ ( 𝑛 Mat 𝑟 ) )
12		vi	⊢ 𝑖
13		vj	⊢ 𝑗
14	12	cv	⊢ 𝑖
15	13	cv	⊢ 𝑗
16	14 15	wne	⊢ 𝑖 ≠ 𝑗
17	5	cv	⊢ 𝑚
18	14 15 17	co	⊢ ( 𝑖 𝑚 𝑗 )
19		c0g	⊢ 0g
20	9 19	cfv	⊢ ( 0g ‘ 𝑟 )
21	18 20	wceq	⊢ ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 )
22	16 21	wi	⊢ ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) )
23	22 13 7	wral	⊢ ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) )
24	23 12 7	wral	⊢ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) )
25	24 5 11	crab	⊢ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) }
26	1 3 2 4 25	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } )
27	0 26	wceq	⊢ DMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } )