Definition df-scmatalt 45740

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-scmatalt	⊢ ScMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))}))

Distinct variable group:   𝑎,𝑐,𝑖,𝑗,𝑚,𝑛,𝑟

Detailed syntax breakdown of Definition df-scmatalt

Step	Hyp	Ref	Expression
1		cscmatalt 45738	. 2 class ScMatALT
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8733	. . 3 class Fin
5		cvv 3432	. . 3 class V
6		va	. . . 4 setvar 𝑎
7	2	cv 1538	. . . . 5 class 𝑛
8	3	cv 1538	. . . . 5 class 𝑟
9		cmat 21554	. . . . 5 class Mat
10	7, 8, 9	co 7275	. . . 4 class (𝑛 Mat 𝑟)
11	6	cv 1538	. . . . 5 class 𝑎
12		vi	. . . . . . . . . . . 12 setvar 𝑖
13	12	cv 1538	. . . . . . . . . . 11 class 𝑖
14		vj	. . . . . . . . . . . 12 setvar 𝑗
15	14	cv 1538	. . . . . . . . . . 11 class 𝑗
16		vm	. . . . . . . . . . . 12 setvar 𝑚
17	16	cv 1538	. . . . . . . . . . 11 class 𝑚
18	13, 15, 17	co 7275	. . . . . . . . . 10 class (𝑖𝑚𝑗)
19	12, 14	weq 1966	. . . . . . . . . . 11 wff 𝑖 = 𝑗
20		vc	. . . . . . . . . . . 12 setvar 𝑐
21	20	cv 1538	. . . . . . . . . . 11 class 𝑐
22		c0g 17150	. . . . . . . . . . . 12 class 0g
23	8, 22	cfv 6433	. . . . . . . . . . 11 class (0g‘𝑟)
24	19, 21, 23	cif 4459	. . . . . . . . . 10 class if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))
25	18, 24	wceq 1539	. . . . . . . . 9 wff (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))
26	25, 14, 7	wral 3064	. . . . . . . 8 wff ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))
27	26, 12, 7	wral 3064	. . . . . . 7 wff ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))
28		cbs 16912	. . . . . . . 8 class Base
29	8, 28	cfv 6433	. . . . . . 7 class (Base‘𝑟)
30	27, 20, 29	wrex 3065	. . . . . 6 wff ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))
31	11, 28	cfv 6433	. . . . . 6 class (Base‘𝑎)
32	30, 16, 31	crab 3068	. . . . 5 class {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))}
33		cress 16941	. . . . 5 class ↾s
34	11, 32, 33	co 7275	. . . 4 class (𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))})
35	6, 10, 34	csb 3832	. . 3 class ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))})
36	2, 3, 4, 5, 35	cmpo 7277	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))}))
37	1, 36	wceq 1539	1 wff ScMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑟))}))

This definition is referenced by: (None)