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