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 , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( 𝑥 · ( 𝑦𝑣 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctimesr .𝑣
1 vx 𝑥
2 cvv V
3 vy 𝑦
4 vv 𝑣
5 cr
6 1 cv 𝑥
7 cmul ·
8 3 cv 𝑦
9 4 cv 𝑣
10 9 8 cfv ( 𝑦𝑣 )
11 6 10 7 co ( 𝑥 · ( 𝑦𝑣 ) )
12 4 5 11 cmpt ( 𝑣 ∈ ℝ ↦ ( 𝑥 · ( 𝑦𝑣 ) ) )
13 1 3 2 2 12 cmpo ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( 𝑥 · ( 𝑦𝑣 ) ) ) )
14 0 13 wceq .𝑣 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( 𝑥 · ( 𝑦𝑣 ) ) ) )