Detailed syntax breakdown of Definition df-madu
Step | Hyp | Ref
| Expression |
1 | | cmadu 21792 |
. 2
class
maAdju |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3431 |
. . 3
class
V |
5 | | vm |
. . . 4
setvar 𝑚 |
6 | 2 | cv 1541 |
. . . . . 6
class 𝑛 |
7 | 3 | cv 1541 |
. . . . . 6
class 𝑟 |
8 | | cmat 21565 |
. . . . . 6
class
Mat |
9 | 6, 7, 8 | co 7272 |
. . . . 5
class (𝑛 Mat 𝑟) |
10 | | cbs 16923 |
. . . . 5
class
Base |
11 | 9, 10 | cfv 6432 |
. . . 4
class
(Base‘(𝑛 Mat
𝑟)) |
12 | | vi |
. . . . 5
setvar 𝑖 |
13 | | vj |
. . . . 5
setvar 𝑗 |
14 | | vk |
. . . . . . 7
setvar 𝑘 |
15 | | vl |
. . . . . . 7
setvar 𝑙 |
16 | 14, 13 | weq 1970 |
. . . . . . . 8
wff 𝑘 = 𝑗 |
17 | 15, 12 | weq 1970 |
. . . . . . . . 9
wff 𝑙 = 𝑖 |
18 | | cur 19748 |
. . . . . . . . . 10
class
1r |
19 | 7, 18 | cfv 6432 |
. . . . . . . . 9
class
(1r‘𝑟) |
20 | | c0g 17161 |
. . . . . . . . . 10
class
0g |
21 | 7, 20 | cfv 6432 |
. . . . . . . . 9
class
(0g‘𝑟) |
22 | 17, 19, 21 | cif 4465 |
. . . . . . . 8
class if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)) |
23 | 14 | cv 1541 |
. . . . . . . . 9
class 𝑘 |
24 | 15 | cv 1541 |
. . . . . . . . 9
class 𝑙 |
25 | 5 | cv 1541 |
. . . . . . . . 9
class 𝑚 |
26 | 23, 24, 25 | co 7272 |
. . . . . . . 8
class (𝑘𝑚𝑙) |
27 | 16, 22, 26 | cif 4465 |
. . . . . . 7
class if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)) |
28 | 14, 15, 6, 6, 27 | cmpo 7274 |
. . . . . 6
class (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))) |
29 | | cmdat 21744 |
. . . . . . 7
class
maDet |
30 | 6, 7, 29 | co 7272 |
. . . . . 6
class (𝑛 maDet 𝑟) |
31 | 28, 30 | cfv 6432 |
. . . . 5
class ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))) |
32 | 12, 13, 6, 6, 31 | cmpo 7274 |
. . . 4
class (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))))) |
33 | 5, 11, 32 | cmpt 5162 |
. . 3
class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))))) |
34 | 2, 3, 4, 4, 33 | cmpo 7274 |
. 2
class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))))))) |
35 | 1, 34 | wceq 1542 |
1
wff maAdju =
(𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))))))) |