Metamath Proof Explorer


Definition df-mulv

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 ) ) ) )

Detailed syntax breakdown

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 ) ) ) )