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

Definition df-dmat 20671
 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 20669 . 2 class DMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8228 . . 3 class Fin
5 cvv 3414 . . 3 class V
6 vi . . . . . . . . 9 setvar 𝑖
76cv 1655 . . . . . . . 8 class 𝑖
8 vj . . . . . . . . 9 setvar 𝑗
98cv 1655 . . . . . . . 8 class 𝑗
107, 9wne 2999 . . . . . . 7 wff 𝑖𝑗
11 vm . . . . . . . . . 10 setvar 𝑚
1211cv 1655 . . . . . . . . 9 class 𝑚
137, 9, 12co 6910 . . . . . . . 8 class (𝑖𝑚𝑗)
143cv 1655 . . . . . . . . 9 class 𝑟
15 c0g 16460 . . . . . . . . 9 class 0g
1614, 15cfv 6127 . . . . . . . 8 class (0g𝑟)
1713, 16wceq 1656 . . . . . . 7 wff (𝑖𝑚𝑗) = (0g𝑟)
1810, 17wi 4 . . . . . 6 wff (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
192cv 1655 . . . . . 6 class 𝑛
2018, 8, 19wral 3117 . . . . 5 wff 𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
2120, 6, 19wral 3117 . . . 4 wff 𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
22 cmat 20587 . . . . . 6 class Mat
2319, 14, 22co 6910 . . . . 5 class (𝑛 Mat 𝑟)
24 cbs 16229 . . . . 5 class Base
2523, 24cfv 6127 . . . 4 class (Base‘(𝑛 Mat 𝑟))
2621, 11, 25crab 3121 . . 3 class {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))}
272, 3, 4, 5, 26cmpt2 6912 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))})
281, 27wceq 1656 1 wff DMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))})
 Colors of variables: wff setvar class This definition is referenced by:  dmatval  20673
 Copyright terms: Public domain W3C validator