Detailed syntax breakdown of Definition df-xps
Step | Hyp | Ref
| Expression |
1 | | cxps 15989 |
. 2
class
×s |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3173 |
. . 3
class
V |
5 | | vx |
. . . . . 6
setvar 𝑥 |
6 | | vy |
. . . . . 6
setvar 𝑦 |
7 | 2 | cv 1474 |
. . . . . . 7
class 𝑟 |
8 | | cbs 15695 |
. . . . . . 7
class
Base |
9 | 7, 8 | cfv 5804 |
. . . . . 6
class
(Base‘𝑟) |
10 | 3 | cv 1474 |
. . . . . . 7
class 𝑠 |
11 | 10, 8 | cfv 5804 |
. . . . . 6
class
(Base‘𝑠) |
12 | 5 | cv 1474 |
. . . . . . . . 9
class 𝑥 |
13 | 12 | csn 4125 |
. . . . . . . 8
class {𝑥} |
14 | 6 | cv 1474 |
. . . . . . . . 9
class 𝑦 |
15 | 14 | csn 4125 |
. . . . . . . 8
class {𝑦} |
16 | | ccda 8872 |
. . . . . . . 8
class
+𝑐 |
17 | 13, 15, 16 | co 6549 |
. . . . . . 7
class ({𝑥} +𝑐 {𝑦}) |
18 | 17 | ccnv 5037 |
. . . . . 6
class ◡({𝑥} +𝑐 {𝑦}) |
19 | 5, 6, 9, 11, 18 | cmpt2 6551 |
. . . . 5
class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) |
20 | 19 | ccnv 5037 |
. . . 4
class ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) |
21 | | csca 15771 |
. . . . . 6
class
Scalar |
22 | 7, 21 | cfv 5804 |
. . . . 5
class
(Scalar‘𝑟) |
23 | 7 | csn 4125 |
. . . . . . 7
class {𝑟} |
24 | 10 | csn 4125 |
. . . . . . 7
class {𝑠} |
25 | 23, 24, 16 | co 6549 |
. . . . . 6
class ({𝑟} +𝑐 {𝑠}) |
26 | 25 | ccnv 5037 |
. . . . 5
class ◡({𝑟} +𝑐 {𝑠}) |
27 | | cprds 15929 |
. . . . 5
class Xs |
28 | 22, 26, 27 | co 6549 |
. . . 4
class
((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠})) |
29 | | cimas 15987 |
. . . 4
class
“s |
30 | 20, 28, 29 | co 6549 |
. . 3
class (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠}))) |
31 | 2, 3, 4, 4, 30 | cmpt2 6551 |
. 2
class (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠})))) |
32 | 1, 31 | wceq 1475 |
1
wff
×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠})))) |