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