Detailed syntax breakdown of Definition df-marepv
Step | Hyp | Ref
| Expression |
1 | | cmatrepV 21704 |
. 2
class
matRepV |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3431 |
. . 3
class
V |
5 | | vm |
. . . 4
setvar 𝑚 |
6 | | vv |
. . . 4
setvar 𝑣 |
7 | 2 | cv 1541 |
. . . . . 6
class 𝑛 |
8 | 3 | cv 1541 |
. . . . . 6
class 𝑟 |
9 | | cmat 21552 |
. . . . . 6
class
Mat |
10 | 7, 8, 9 | co 7271 |
. . . . 5
class (𝑛 Mat 𝑟) |
11 | | cbs 16910 |
. . . . 5
class
Base |
12 | 10, 11 | cfv 6432 |
. . . 4
class
(Base‘(𝑛 Mat
𝑟)) |
13 | 8, 11 | cfv 6432 |
. . . . 5
class
(Base‘𝑟) |
14 | | cmap 8598 |
. . . . 5
class
↑m |
15 | 13, 7, 14 | co 7271 |
. . . 4
class
((Base‘𝑟)
↑m 𝑛) |
16 | | vk |
. . . . 5
setvar 𝑘 |
17 | | vi |
. . . . . 6
setvar 𝑖 |
18 | | vj |
. . . . . 6
setvar 𝑗 |
19 | 18, 16 | weq 1970 |
. . . . . . 7
wff 𝑗 = 𝑘 |
20 | 17 | cv 1541 |
. . . . . . . 8
class 𝑖 |
21 | 6 | cv 1541 |
. . . . . . . 8
class 𝑣 |
22 | 20, 21 | cfv 6432 |
. . . . . . 7
class (𝑣‘𝑖) |
23 | 18 | cv 1541 |
. . . . . . . 8
class 𝑗 |
24 | 5 | cv 1541 |
. . . . . . . 8
class 𝑚 |
25 | 20, 23, 24 | co 7271 |
. . . . . . 7
class (𝑖𝑚𝑗) |
26 | 19, 22, 25 | cif 4465 |
. . . . . 6
class if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗)) |
27 | 17, 18, 7, 7, 26 | cmpo 7273 |
. . . . 5
class (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗))) |
28 | 16, 7, 27 | cmpt 5162 |
. . . 4
class (𝑘 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗)))) |
29 | 5, 6, 12, 15, 28 | cmpo 7273 |
. . 3
class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗))))) |
30 | 2, 3, 4, 4, 29 | cmpo 7273 |
. 2
class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗)))))) |
31 | 1, 30 | wceq 1542 |
1
wff matRepV =
(𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗)))))) |