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 ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁢ y ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctimesr class ⋅ 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 ×
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 ∈ ℝ ⟼ x ⁢ y ⁡ v
13 1 3 2 2 12 cmpo class x ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁢ y ⁡ v
14 0 13 wceq wff ⋅ v = x ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁢ y ⁡ v