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⟼⦋nMatr/a⦌a↾𝑠m∈Basea|∃c∈Baser∀i∈n∀j∈nimj=ifi=jc0r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cscmatalt classScMatALT
1 vn setvarn
2 cfn classFin
3 vr setvarr
4 cvv classV
5 1 cv setvarn
6 cmat classMat
7 3 cv setvarr
8 5 7 6 co classnMatr
9 va setvara
10 9 cv setvara
11 cress class↾𝑠
12 vm setvarm
13 cbs classBase
14 10 13 cfv classBasea
15 vc setvarc
16 7 13 cfv classBaser
17 vi setvari
18 vj setvarj
19 17 cv setvari
20 12 cv setvarm
21 18 cv setvarj
22 19 21 20 co classimj
23 19 21 wceq wffi=j
24 15 cv setvarc
25 c0g class0𝑔
26 7 25 cfv class0r
27 23 24 26 cif classifi=jc0r
28 22 27 wceq wffimj=ifi=jc0r
29 28 18 5 wral wff∀j∈nimj=ifi=jc0r
30 29 17 5 wral wff∀i∈n∀j∈nimj=ifi=jc0r
31 30 15 16 wrex wff∃c∈Baser∀i∈n∀j∈nimj=ifi=jc0r
32 31 12 14 crab classm∈Basea|∃c∈Baser∀i∈n∀j∈nimj=ifi=jc0r
33 10 32 11 co classa↾𝑠m∈Basea|∃c∈Baser∀i∈n∀j∈nimj=ifi=jc0r
34 9 8 33 csb class⦋nMatr/a⦌a↾𝑠m∈Basea|∃c∈Baser∀i∈n∀j∈nimj=ifi=jc0r
35 1 3 2 4 34 cmpo classn∈Fin,r∈V⟼⦋nMatr/a⦌a↾𝑠m∈Basea|∃c∈Baser∀i∈n∀j∈nimj=ifi=jc0r
36 0 35 wceq wffScMatALT=n∈Fin,r∈V⟼⦋nMatr/a⦌a↾𝑠m∈Basea|∃c∈Baser∀i∈n∀j∈nimj=ifi=jc0r