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

Definition df-scmat 20064
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-scmat ScMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))})
Distinct variable group:   𝑎,𝑐,𝑚,𝑛,𝑟

Detailed syntax breakdown of Definition df-scmat
StepHypRef Expression
1 cscmat 20062 . 2 class ScMat
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cfn 7819 . . 3 class Fin
5 cvv 3173 . . 3 class V
6 va . . . 4 setvar 𝑎
72cv 1474 . . . . 5 class 𝑛
83cv 1474 . . . . 5 class 𝑟
9 cmat 19980 . . . . 5 class Mat
107, 8, 9co 6527 . . . 4 class (𝑛 Mat 𝑟)
11 vm . . . . . . . 8 setvar 𝑚
1211cv 1474 . . . . . . 7 class 𝑚
13 vc . . . . . . . . 9 setvar 𝑐
1413cv 1474 . . . . . . . 8 class 𝑐
156cv 1474 . . . . . . . . 9 class 𝑎
16 cur 18273 . . . . . . . . 9 class 1r
1715, 16cfv 5790 . . . . . . . 8 class (1r𝑎)
18 cvsca 15721 . . . . . . . . 9 class ·𝑠
1915, 18cfv 5790 . . . . . . . 8 class ( ·𝑠𝑎)
2014, 17, 19co 6527 . . . . . . 7 class (𝑐( ·𝑠𝑎)(1r𝑎))
2112, 20wceq 1475 . . . . . 6 wff 𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))
22 cbs 15644 . . . . . . 7 class Base
238, 22cfv 5790 . . . . . 6 class (Base‘𝑟)
2421, 13, 23wrex 2897 . . . . 5 wff 𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))
2515, 22cfv 5790 . . . . 5 class (Base‘𝑎)
2624, 11, 25crab 2900 . . . 4 class {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))}
276, 10, 26csb 3499 . . 3 class (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))}
282, 3, 4, 5, 27cmpt2 6529 . 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))})
291, 28wceq 1475 1 wff ScMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑛 Mat 𝑟) / 𝑎{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠𝑎)(1r𝑎))})
Colors of variables: wff setvar class
This definition is referenced by:  scmatval  20077
  Copyright terms: Public domain W3C validator