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