Metamath Proof Explorer

Definition df-scmat

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-scmat ⊢ ScMat = n ∈ Fin , r ∈ V ⟼ ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cscmat class ScMat
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 vm setvar m
11 cbs class Base
12 9 cv setvar a
13 12 11 cfv class Base a
14 vc setvar c
15 7 11 cfv class Base r
16 10 cv setvar m
17 14 cv setvar c
18 cvsca class ⋅ 𝑠
19 12 18 cfv class ⋅ a
20 cur class 1 r
21 12 20 cfv class 1 a
22 17 21 19 co class c ⋅ a 1 a
23 16 22 wceq wff m = c ⋅ a 1 a
24 23 14 15 wrex wff ∃ c ∈ Base r m = c ⋅ a 1 a
25 24 10 13 crab class m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a
26 9 8 25 csb class ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a
27 1 3 2 4 26 cmpo class n ∈ Fin , r ∈ V ⟼ ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a
28 0 27 wceq wff ScMat = n ∈ Fin , r ∈ V ⟼ ⦋ n Mat r / a⦌ m ∈ Base a | ∃ c ∈ Base r m = c ⋅ a 1 a