MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dmat Structured version   Visualization version   GIF version

Definition df-dmat 20057
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
StepHypRef Expression
1 cdmat 20055 . 2 class DMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 7818 . . 3 class Fin
5 cvv 3172 . . 3 class V
6 vi . . . . . . . . 9 setvar 𝑖
76cv 1473 . . . . . . . 8 class 𝑖
8 vj . . . . . . . . 9 setvar 𝑗
98cv 1473 . . . . . . . 8 class 𝑗
107, 9wne 2779 . . . . . . 7 wff 𝑖𝑗
11 vm . . . . . . . . . 10 setvar 𝑚
1211cv 1473 . . . . . . . . 9 class 𝑚
137, 9, 12co 6527 . . . . . . . 8 class (𝑖𝑚𝑗)
143cv 1473 . . . . . . . . 9 class 𝑟
15 c0g 15869 . . . . . . . . 9 class 0g
1614, 15cfv 5790 . . . . . . . 8 class (0g𝑟)
1713, 16wceq 1474 . . . . . . 7 wff (𝑖𝑚𝑗) = (0g𝑟)
1810, 17wi 4 . . . . . 6 wff (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
192cv 1473 . . . . . 6 class 𝑛
2018, 8, 19wral 2895 . . . . 5 wff 𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
2120, 6, 19wral 2895 . . . 4 wff 𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
22 cmat 19974 . . . . . 6 class Mat
2319, 14, 22co 6527 . . . . 5 class (𝑛 Mat 𝑟)
24 cbs 15641 . . . . 5 class Base
2523, 24cfv 5790 . . . 4 class (Base‘(𝑛 Mat 𝑟))
2621, 11, 25crab 2899 . . 3 class {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))}
272, 3, 4, 5, 26cmpt2 6529 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))})
281, 27wceq 1474 1 wff DMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))})
Colors of variables: wff setvar class
This definition is referenced by:  dmatval  20059
  Copyright terms: Public domain W3C validator