Definition df-dmat 22496

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.)

Assertion

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

Distinct variable group:   𝑖,𝑗,𝑚,𝑛,𝑟

Detailed syntax breakdown of Definition df-dmat

Step	Hyp	Ref	Expression
1		cdmat 22494	. 2 class DMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8985	. . 3 class Fin
5		cvv 3480	. . 3 class V
6		vi	. . . . . . . . 9 setvar 𝑖
7	6	cv 1539	. . . . . . . 8 class 𝑖
8		vj	. . . . . . . . 9 setvar 𝑗
9	8	cv 1539	. . . . . . . 8 class 𝑗
10	7, 9	wne 2940	. . . . . . 7 wff 𝑖 ≠ 𝑗
11		vm	. . . . . . . . . 10 setvar 𝑚
12	11	cv 1539	. . . . . . . . 9 class 𝑚
13	7, 9, 12	co 7431	. . . . . . . 8 class (𝑖𝑚𝑗)
14	3	cv 1539	. . . . . . . . 9 class 𝑟
15		c0g 17484	. . . . . . . . 9 class 0g
16	14, 15	cfv 6561	. . . . . . . 8 class (0g‘𝑟)
17	13, 16	wceq 1540	. . . . . . 7 wff (𝑖𝑚𝑗) = (0g‘𝑟)
18	10, 17	wi 4	. . . . . 6 wff (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))
19	2	cv 1539	. . . . . 6 class 𝑛
20	18, 8, 19	wral 3061	. . . . 5 wff ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))
21	20, 6, 19	wral 3061	. . . 4 wff ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))
22		cmat 22411	. . . . . 6 class Mat
23	19, 14, 22	co 7431	. . . . 5 class (𝑛 Mat 𝑟)
24		cbs 17247	. . . . 5 class Base
25	23, 24	cfv 6561	. . . 4 class (Base‘(𝑛 Mat 𝑟))
26	21, 11, 25	crab 3436	. . 3 class {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}
27	2, 3, 4, 5, 26	cmpo 7433	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))})
28	1, 27	wceq 1540	1 wff DMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))})

This definition is referenced by:  dmatval  22498