Metamath Proof Explorer

Definition df-dmatalt

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-dmatalt ⊢ DMatALT = n ∈ Fin , r ∈ V ⟼ ⦋ n Mat r / a⦌ a ↾ 𝑠 m ∈ Base a | ∀ i ∈ n ∀ j ∈ n i ≠ j → i m j = 0 r

Detailed syntax breakdown

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