Definition df-scmat 22497

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 22495	. 2 class ScMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8985	. . 3 class Fin
5		cvv 3480	. . 3 class V
6		va	. . . 4 setvar 𝑎
7	2	cv 1539	. . . . 5 class 𝑛
8	3	cv 1539	. . . . 5 class 𝑟
9		cmat 22411	. . . . 5 class Mat
10	7, 8, 9	co 7431	. . . 4 class (𝑛 Mat 𝑟)
11		vm	. . . . . . . 8 setvar 𝑚
12	11	cv 1539	. . . . . . 7 class 𝑚
13		vc	. . . . . . . . 9 setvar 𝑐
14	13	cv 1539	. . . . . . . 8 class 𝑐
15	6	cv 1539	. . . . . . . . 9 class 𝑎
16		cur 20178	. . . . . . . . 9 class 1r
17	15, 16	cfv 6561	. . . . . . . 8 class (1r‘𝑎)
18		cvsca 17301	. . . . . . . . 9 class ·𝑠
19	15, 18	cfv 6561	. . . . . . . 8 class ( ·𝑠 ‘𝑎)
20	14, 17, 19	co 7431	. . . . . . 7 class (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))
21	12, 20	wceq 1540	. . . . . 6 wff 𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))
22		cbs 17247	. . . . . . 7 class Base
23	8, 22	cfv 6561	. . . . . 6 class (Base‘𝑟)
24	21, 13, 23	wrex 3070	. . . . 5 wff ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))
25	15, 22	cfv 6561	. . . . 5 class (Base‘𝑎)
26	24, 11, 25	crab 3436	. . . 4 class {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))}
27	6, 10, 26	csb 3899	. . 3 class ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))}
28	2, 3, 4, 5, 27	cmpo 7433	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))})
29	1, 28	wceq 1540	1 wff ScMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))})

This definition is referenced by:  scmatval  22510