Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dmatalt Structured version   Visualization version   GIF version

Definition df-dmatalt 42712
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-dmatalt DMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))}))
Distinct variable group:   𝑖,𝑎,𝑗,𝑚,𝑛,𝑟

Detailed syntax breakdown of Definition df-dmatalt
StepHypRef Expression
1 cdmatalt 42710 . 2 class DMatALT
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8113 . . 3 class Fin
5 cvv 3351 . . 3 class V
6 va . . . 4 setvar 𝑎
72cv 1630 . . . . 5 class 𝑛
83cv 1630 . . . . 5 class 𝑟
9 cmat 20430 . . . . 5 class Mat
107, 8, 9co 6796 . . . 4 class (𝑛 Mat 𝑟)
116cv 1630 . . . . 5 class 𝑎
12 vi . . . . . . . . . . 11 setvar 𝑖
1312cv 1630 . . . . . . . . . 10 class 𝑖
14 vj . . . . . . . . . . 11 setvar 𝑗
1514cv 1630 . . . . . . . . . 10 class 𝑗
1613, 15wne 2943 . . . . . . . . 9 wff 𝑖𝑗
17 vm . . . . . . . . . . . 12 setvar 𝑚
1817cv 1630 . . . . . . . . . . 11 class 𝑚
1913, 15, 18co 6796 . . . . . . . . . 10 class (𝑖𝑚𝑗)
20 c0g 16308 . . . . . . . . . . 11 class 0g
218, 20cfv 6030 . . . . . . . . . 10 class (0g𝑟)
2219, 21wceq 1631 . . . . . . . . 9 wff (𝑖𝑚𝑗) = (0g𝑟)
2316, 22wi 4 . . . . . . . 8 wff (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
2423, 14, 7wral 3061 . . . . . . 7 wff 𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
2524, 12, 7wral 3061 . . . . . 6 wff 𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))
26 cbs 16064 . . . . . . 7 class Base
2711, 26cfv 6030 . . . . . 6 class (Base‘𝑎)
2825, 17, 27crab 3065 . . . . 5 class {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))}
29 cress 16065 . . . . 5 class s
3011, 28, 29co 6796 . . . 4 class (𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))})
316, 10, 30csb 3682 . . 3 class (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))})
322, 3, 4, 5, 31cmpt2 6798 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))}))
331, 32wceq 1631 1 wff DMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖𝑛𝑗𝑛 (𝑖𝑗 → (𝑖𝑚𝑗) = (0g𝑟))}))
Colors of variables: wff setvar class
This definition is referenced by:  dmatALTval  42714
  Copyright terms: Public domain W3C validator