Detailed syntax breakdown of Definition df-mvmul
Step | Hyp | Ref
| Expression |
1 | | cmvmul 21670 |
. 2
class
maVecMul |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vo |
. . 3
setvar 𝑜 |
4 | | cvv 3430 |
. . 3
class
V |
5 | | vm |
. . . 4
setvar 𝑚 |
6 | 3 | cv 1540 |
. . . . 5
class 𝑜 |
7 | | c1st 7815 |
. . . . 5
class
1st |
8 | 6, 7 | cfv 6430 |
. . . 4
class
(1st ‘𝑜) |
9 | | vn |
. . . . 5
setvar 𝑛 |
10 | | c2nd 7816 |
. . . . . 6
class
2nd |
11 | 6, 10 | cfv 6430 |
. . . . 5
class
(2nd ‘𝑜) |
12 | | vx |
. . . . . 6
setvar 𝑥 |
13 | | vy |
. . . . . 6
setvar 𝑦 |
14 | 2 | cv 1540 |
. . . . . . . 8
class 𝑟 |
15 | | cbs 16893 |
. . . . . . . 8
class
Base |
16 | 14, 15 | cfv 6430 |
. . . . . . 7
class
(Base‘𝑟) |
17 | 5 | cv 1540 |
. . . . . . . 8
class 𝑚 |
18 | 9 | cv 1540 |
. . . . . . . 8
class 𝑛 |
19 | 17, 18 | cxp 5586 |
. . . . . . 7
class (𝑚 × 𝑛) |
20 | | cmap 8589 |
. . . . . . 7
class
↑m |
21 | 16, 19, 20 | co 7268 |
. . . . . 6
class
((Base‘𝑟)
↑m (𝑚
× 𝑛)) |
22 | 16, 18, 20 | co 7268 |
. . . . . 6
class
((Base‘𝑟)
↑m 𝑛) |
23 | | vi |
. . . . . . 7
setvar 𝑖 |
24 | | vj |
. . . . . . . . 9
setvar 𝑗 |
25 | 23 | cv 1540 |
. . . . . . . . . . 11
class 𝑖 |
26 | 24 | cv 1540 |
. . . . . . . . . . 11
class 𝑗 |
27 | 12 | cv 1540 |
. . . . . . . . . . 11
class 𝑥 |
28 | 25, 26, 27 | co 7268 |
. . . . . . . . . 10
class (𝑖𝑥𝑗) |
29 | 13 | cv 1540 |
. . . . . . . . . . 11
class 𝑦 |
30 | 26, 29 | cfv 6430 |
. . . . . . . . . 10
class (𝑦‘𝑗) |
31 | | cmulr 16944 |
. . . . . . . . . . 11
class
.r |
32 | 14, 31 | cfv 6430 |
. . . . . . . . . 10
class
(.r‘𝑟) |
33 | 28, 30, 32 | co 7268 |
. . . . . . . . 9
class ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)) |
34 | 24, 18, 33 | cmpt 5161 |
. . . . . . . 8
class (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))) |
35 | | cgsu 17132 |
. . . . . . . 8
class
Σg |
36 | 14, 34, 35 | co 7268 |
. . . . . . 7
class (𝑟 Σg
(𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))) |
37 | 23, 17, 36 | cmpt 5161 |
. . . . . 6
class (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))) |
38 | 12, 13, 21, 22, 37 | cmpo 7270 |
. . . . 5
class (𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) |
39 | 9, 11, 38 | csb 3836 |
. . . 4
class
⦋(2nd ‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) |
40 | 5, 8, 39 | csb 3836 |
. . 3
class
⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd
‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))) |
41 | 2, 3, 4, 4, 40 | cmpo 7270 |
. 2
class (𝑟 ∈ V, 𝑜 ∈ V ↦
⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd
‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))) |
42 | 1, 41 | wceq 1541 |
1
wff maVecMul =
(𝑟 ∈ V, 𝑜 ∈ V ↦
⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd
‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))) |