Metamath Proof Explorer


Definition df-scmatalt

Description: Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in Connell p. 57: "Ascalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cI_n". (Contributed by AV, 8-Dec-2019)

Ref Expression
Assertion df-scmatalt ScMatALT = n Fin , r V n Mat r / a a 𝑠 m Base a | c Base r i n j n i m j = if i = j c 0 r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cscmatalt class ScMatALT
1 vn setvar n
2 cfn class Fin
3 vr setvar r
4 cvv class V
5 1 cv setvar n
6 cmat class Mat
7 3 cv setvar r
8 5 7 6 co class n Mat r
9 va setvar a
10 9 cv setvar a
11 cress class 𝑠
12 vm setvar m
13 cbs class Base
14 10 13 cfv class Base a
15 vc setvar c
16 7 13 cfv class Base r
17 vi setvar i
18 vj setvar j
19 17 cv setvar i
20 12 cv setvar m
21 18 cv setvar j
22 19 21 20 co class i m j
23 19 21 wceq wff i = j
24 15 cv setvar c
25 c0g class 0 𝑔
26 7 25 cfv class 0 r
27 23 24 26 cif class if i = j c 0 r
28 22 27 wceq wff i m j = if i = j c 0 r
29 28 18 5 wral wff j n i m j = if i = j c 0 r
30 29 17 5 wral wff i n j n i m j = if i = j c 0 r
31 30 15 16 wrex wff c Base r i n j n i m j = if i = j c 0 r
32 31 12 14 crab class m Base a | c Base r i n j n i m j = if i = j c 0 r
33 10 32 11 co class a 𝑠 m Base a | c Base r i n j n i m j = if i = j c 0 r
34 9 8 33 csb class n Mat r / a a 𝑠 m Base a | c Base r i n j n i m j = if i = j c 0 r
35 1 3 2 4 34 cmpo class n Fin , r V n Mat r / a a 𝑠 m Base a | c Base r i n j n i m j = if i = j c 0 r
36 0 35 wceq wff ScMatALT = n Fin , r V n Mat r / a a 𝑠 m Base a | c Base r i n j n i m j = if i = j c 0 r