Definition df-dmatalt 45627

Description: Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in [Roman] p. 4 or Definition 3.12 in [Hefferon] p. 240. (Contributed by AV, 8-Dec-2019.)

Assertion

Ref	Expression
df-dmatalt	⊢ DMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}))

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

Detailed syntax breakdown of Definition df-dmatalt

Step	Hyp	Ref	Expression
1		cdmatalt 45625	. 2 class DMatALT
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cfn 8691	. . 3 class Fin
5		cvv 3422	. . 3 class V
6		va	. . . 4 setvar 𝑎
7	2	cv 1538	. . . . 5 class 𝑛
8	3	cv 1538	. . . . 5 class 𝑟
9		cmat 21464	. . . . 5 class Mat
10	7, 8, 9	co 7255	. . . 4 class (𝑛 Mat 𝑟)
11	6	cv 1538	. . . . 5 class 𝑎
12		vi	. . . . . . . . . . 11 setvar 𝑖
13	12	cv 1538	. . . . . . . . . 10 class 𝑖
14		vj	. . . . . . . . . . 11 setvar 𝑗
15	14	cv 1538	. . . . . . . . . 10 class 𝑗
16	13, 15	wne 2942	. . . . . . . . 9 wff 𝑖 ≠ 𝑗
17		vm	. . . . . . . . . . . 12 setvar 𝑚
18	17	cv 1538	. . . . . . . . . . 11 class 𝑚
19	13, 15, 18	co 7255	. . . . . . . . . 10 class (𝑖𝑚𝑗)
20		c0g 17067	. . . . . . . . . . 11 class 0g
21	8, 20	cfv 6418	. . . . . . . . . 10 class (0g‘𝑟)
22	19, 21	wceq 1539	. . . . . . . . 9 wff (𝑖𝑚𝑗) = (0g‘𝑟)
23	16, 22	wi 4	. . . . . . . 8 wff (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))
24	23, 14, 7	wral 3063	. . . . . . 7 wff ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))
25	24, 12, 7	wral 3063	. . . . . 6 wff ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))
26		cbs 16840	. . . . . . 7 class Base
27	11, 26	cfv 6418	. . . . . 6 class (Base‘𝑎)
28	25, 17, 27	crab 3067	. . . . 5 class {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}
29		cress 16867	. . . . 5 class ↾s
30	11, 28, 29	co 7255	. . . 4 class (𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))})
31	6, 10, 30	csb 3828	. . 3 class ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))})
32	2, 3, 4, 5, 31	cmpo 7257	. 2 class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}))
33	1, 32	wceq 1539	1 wff DMatALT = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌(𝑎 ↾s {𝑚 ∈ (Base‘𝑎) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}))

This definition is referenced by:  dmatALTval  45629