Definition df-addr

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

	Ref	Expression
Assertion	df-addr	⊢ +𝑟 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( ( 𝑥 ‘ 𝑣 ) + ( 𝑦 ‘ 𝑣 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplusr	⊢ +𝑟
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		vv	⊢ 𝑣
5		cr	⊢ ℝ
6	1	cv	⊢ 𝑥
7	4	cv	⊢ 𝑣
8	7 6	cfv	⊢ ( 𝑥 ‘ 𝑣 )
9		caddc	⊢ +
10	3	cv	⊢ 𝑦
11	7 10	cfv	⊢ ( 𝑦 ‘ 𝑣 )
12	8 11 9	co	⊢ ( ( 𝑥 ‘ 𝑣 ) + ( 𝑦 ‘ 𝑣 ) )
13	4 5 12	cmpt	⊢ ( 𝑣 ∈ ℝ ↦ ( ( 𝑥 ‘ 𝑣 ) + ( 𝑦 ‘ 𝑣 ) ) )
14	1 3 2 2 13	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( ( 𝑥 ‘ 𝑣 ) + ( 𝑦 ‘ 𝑣 ) ) ) )
15	0 14	wceq	⊢ +𝑟 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( ( 𝑥 ‘ 𝑣 ) + ( 𝑦 ‘ 𝑣 ) ) ) )