Detailed syntax breakdown of Definition df-dmat
Step | Hyp | Ref
| Expression |
1 | | cdmat 21417 |
. 2
class
DMat |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cfn 8650 |
. . 3
class
Fin |
5 | | cvv 3423 |
. . 3
class
V |
6 | | vi |
. . . . . . . . 9
setvar 𝑖 |
7 | 6 | cv 1542 |
. . . . . . . 8
class 𝑖 |
8 | | vj |
. . . . . . . . 9
setvar 𝑗 |
9 | 8 | cv 1542 |
. . . . . . . 8
class 𝑗 |
10 | 7, 9 | wne 2943 |
. . . . . . 7
wff 𝑖 ≠ 𝑗 |
11 | | vm |
. . . . . . . . . 10
setvar 𝑚 |
12 | 11 | cv 1542 |
. . . . . . . . 9
class 𝑚 |
13 | 7, 9, 12 | co 7235 |
. . . . . . . 8
class (𝑖𝑚𝑗) |
14 | 3 | cv 1542 |
. . . . . . . . 9
class 𝑟 |
15 | | c0g 16977 |
. . . . . . . . 9
class
0g |
16 | 14, 15 | cfv 6401 |
. . . . . . . 8
class
(0g‘𝑟) |
17 | 13, 16 | wceq 1543 |
. . . . . . 7
wff (𝑖𝑚𝑗) = (0g‘𝑟) |
18 | 10, 17 | wi 4 |
. . . . . 6
wff (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟)) |
19 | 2 | cv 1542 |
. . . . . 6
class 𝑛 |
20 | 18, 8, 19 | wral 3064 |
. . . . 5
wff
∀𝑗 ∈
𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟)) |
21 | 20, 6, 19 | wral 3064 |
. . . 4
wff
∀𝑖 ∈
𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟)) |
22 | | cmat 21336 |
. . . . . 6
class
Mat |
23 | 19, 14, 22 | co 7235 |
. . . . 5
class (𝑛 Mat 𝑟) |
24 | | cbs 16793 |
. . . . 5
class
Base |
25 | 23, 24 | cfv 6401 |
. . . 4
class
(Base‘(𝑛 Mat
𝑟)) |
26 | 21, 11, 25 | crab 3068 |
. . 3
class {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))} |
27 | 2, 3, 4, 5, 26 | cmpo 7237 |
. 2
class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}) |
28 | 1, 27 | wceq 1543 |
1
wff DMat =
(𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))}) |