Description: Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | df-mulv | |- .v = ( x e. _V , y e. _V |-> ( v e. RR |-> ( x x. ( y ` v ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ctimesr | |- .v |
|
1 | vx | |- x |
|
2 | cvv | |- _V |
|
3 | vy | |- y |
|
4 | vv | |- v |
|
5 | cr | |- RR |
|
6 | 1 | cv | |- x |
7 | cmul | |- x. |
|
8 | 3 | cv | |- y |
9 | 4 | cv | |- v |
10 | 9 8 | cfv | |- ( y ` v ) |
11 | 6 10 7 | co | |- ( x x. ( y ` v ) ) |
12 | 4 5 11 | cmpt | |- ( v e. RR |-> ( x x. ( y ` v ) ) ) |
13 | 1 3 2 2 12 | cmpo | |- ( x e. _V , y e. _V |-> ( v e. RR |-> ( x x. ( y ` v ) ) ) ) |
14 | 0 13 | wceq | |- .v = ( x e. _V , y e. _V |-> ( v e. RR |-> ( x x. ( y ` v ) ) ) ) |