df-mulv

Description: Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012)

		Ref	Expression
	Assertion	df-mulv	$⊢ \cdot_{v} = (x \in V, y \in V ⟼ (v \in ℝ ⟼ x y (v)))$

Step	Hyp	Ref	Expression
0		ctimesr	$class \cdot_{v}$
1		vx	$setvar x$
2		cvv	$class V$
3		vy	$setvar y$
4		vv	$setvar v$
5		cr	$class ℝ$
6	1	cv	$setvar x$
7		cmul	$class \times$
8	3	cv	$setvar y$
9	4	cv	$setvar v$
10	9 8	cfv	$class y (v)$
11	6 10 7	co	$class x y (v)$
12	4 5 11	cmpt	$class (v \in ℝ ⟼ x y (v))$
13	1 3 2 2 12	cmpo	$class (x \in V, y \in V ⟼ (v \in ℝ ⟼ x y (v)))$
14	0 13	wceq	$wff \cdot_{v} = (x \in V, y \in V ⟼ (v \in ℝ ⟼ x y (v)))$

Metamath Proof Explorer