Description: Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | df-mulv | ⊢ .𝑣 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( 𝑥 · ( 𝑦 ‘ 𝑣 ) ) ) ) |
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 ↦ ( 𝑣 ∈ ℝ ↦ ( 𝑥 · ( 𝑦 ‘ 𝑣 ) ) ) ) |