Metamath Proof Explorer

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 = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r | ∀ i ∈ n ∀ j ∈ n i ≠ j → i m j = 0 r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdmat class DMat
1 vn setvar n
2 cfn class Fin
3 vr setvar r
4 cvv class V
5 vm setvar m
6 cbs class Base
7 1 cv setvar n
8 cmat class Mat
9 3 cv setvar r
10 7 9 8 co class n Mat r
11 10 6 cfv class Base n Mat r
12 vi setvar i
13 vj setvar j
14 12 cv setvar i
15 13 cv setvar j
16 14 15 wne wff i ≠ j
17 5 cv setvar m
18 14 15 17 co class i m j
19 c0g class 0 𝑔
20 9 19 cfv class 0 r
21 18 20 wceq wff i m j = 0 r
22 16 21 wi wff i ≠ j → i m j = 0 r
23 22 13 7 wral wff ∀ j ∈ n i ≠ j → i m j = 0 r
24 23 12 7 wral wff ∀ i ∈ n ∀ j ∈ n i ≠ j → i m j = 0 r
25 24 5 11 crab class m ∈ Base n Mat r | ∀ i ∈ n ∀ j ∈ n i ≠ j → i m j = 0 r
26 1 3 2 4 25 cmpo class n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r | ∀ i ∈ n ∀ j ∈ n i ≠ j → i m j = 0 r
27 0 26 wceq wff DMat = n ∈ Fin , r ∈ V ⟼ m ∈ Base n Mat r | ∀ i ∈ n ∀ j ∈ n i ≠ j → i m j = 0 r