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

Definition df-scmatalt 43053
 Description: Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in [Connell] p. 57: "A scalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cIn";. (Contributed by AV, 8-Dec-2019.)
Assertion
Ref Expression
df-scmatalt ScMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))}))
Distinct variable group:   𝑎,𝑐,𝑖,𝑗,𝑚,𝑛,𝑟

Detailed syntax breakdown of Definition df-scmatalt
StepHypRef Expression
1 cscmatalt 43051 . 2 class ScMatALT
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 8228 . . 3 class Fin
5 cvv 3414 . . 3 class V
6 va . . . 4 setvar 𝑎
72cv 1655 . . . . 5 class 𝑛
83cv 1655 . . . . 5 class 𝑟
9 cmat 20587 . . . . 5 class Mat
107, 8, 9co 6910 . . . 4 class (𝑛 Mat 𝑟)
116cv 1655 . . . . 5 class 𝑎
12 vi . . . . . . . . . . . 12 setvar 𝑖
1312cv 1655 . . . . . . . . . . 11 class 𝑖
14 vj . . . . . . . . . . . 12 setvar 𝑗
1514cv 1655 . . . . . . . . . . 11 class 𝑗
16 vm . . . . . . . . . . . 12 setvar 𝑚
1716cv 1655 . . . . . . . . . . 11 class 𝑚
1813, 15, 17co 6910 . . . . . . . . . 10 class (𝑖𝑚𝑗)
1912, 14weq 2061 . . . . . . . . . . 11 wff 𝑖 = 𝑗
20 vc . . . . . . . . . . . 12 setvar 𝑐
2120cv 1655 . . . . . . . . . . 11 class 𝑐
22 c0g 16460 . . . . . . . . . . . 12 class 0g
238, 22cfv 6127 . . . . . . . . . . 11 class (0g𝑟)
2419, 21, 23cif 4308 . . . . . . . . . 10 class if(𝑖 = 𝑗, 𝑐, (0g𝑟))
2518, 24wceq 1656 . . . . . . . . 9 wff (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))
2625, 14, 7wral 3117 . . . . . . . 8 wff 𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))
2726, 12, 7wral 3117 . . . . . . 7 wff 𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))
28 cbs 16229 . . . . . . . 8 class Base
298, 28cfv 6127 . . . . . . 7 class (Base‘𝑟)
3027, 20, 29wrex 3118 . . . . . 6 wff 𝑐 ∈ (Base‘𝑟)∀𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))
3111, 28cfv 6127 . . . . . 6 class (Base‘𝑎)
3230, 16, 31crab 3121 . . . . 5 class {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))}
33 cress 16230 . . . . 5 class s
3411, 32, 33co 6910 . . . 4 class (𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))})
356, 10, 34csb 3757 . . 3 class (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))})
362, 3, 4, 5, 35cmpt2 6912 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))}))
371, 36wceq 1656 1 wff ScMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎(𝑎s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖𝑛𝑗𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g𝑟))}))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator