Definition df-scmat 21975

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 cI_n";. (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

Step	Hyp	Ref	Expression
1		cscmat 21973	. 2 class ScMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8935	. . 3 class Fin
5		cvv 3475	. . 3 class V
6		va	. . . 4 setvar 𝑎
7	2	cv 1541	. . . . 5 class 𝑛
8	3	cv 1541	. . . . 5 class 𝑟
9		cmat 21889	. . . . 5 class Mat
10	7, 8, 9	co 7404	. . . 4 class (𝑛 Mat 𝑟)
11		vm	. . . . . . . 8 setvar 𝑚
12	11	cv 1541	. . . . . . 7 class 𝑚
13		vc	. . . . . . . . 9 setvar 𝑐
14	13	cv 1541	. . . . . . . 8 class 𝑐
15	6	cv 1541	. . . . . . . . 9 class 𝑎
16		cur 19996	. . . . . . . . 9 class 1r
17	15, 16	cfv 6540	. . . . . . . 8 class (1r‘𝑎)
18		cvsca 17197	. . . . . . . . 9 class ·𝑠
19	15, 18	cfv 6540	. . . . . . . 8 class ( ·𝑠 ‘𝑎)
20	14, 17, 19	co 7404	. . . . . . 7 class (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))
21	12, 20	wceq 1542	. . . . . 6 wff 𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))
22		cbs 17140	. . . . . . 7 class Base
23	8, 22	cfv 6540	. . . . . 6 class (Base‘𝑟)
24	21, 13, 23	wrex 3071	. . . . 5 wff ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))
25	15, 22	cfv 6540	. . . . 5 class (Base‘𝑎)
26	24, 11, 25	crab 3433	. . . 4 class {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))}
27	6, 10, 26	csb 3892	. . 3 class ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))}
28	2, 3, 4, 5, 27	cmpo 7406	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))})
29	1, 28	wceq 1542	1 wff ScMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))})

This definition is referenced by:  scmatval  21988