Metamath Proof Explorer


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