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 ⊢ + r = x ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁡ v + y ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplusr class + r
1 vx setvar x
2 cvv class V
3 vy setvar y
4 vv setvar v
5 cr class ℝ
6 1 cv setvar x
7 4 cv setvar v
8 7 6 cfv class x ⁡ v
9 caddc class +
10 3 cv setvar y
11 7 10 cfv class y ⁡ v
12 8 11 9 co class x ⁡ v + y ⁡ v
13 4 5 12 cmpt class v ∈ ℝ ⟼ x ⁡ v + y ⁡ v
14 1 3 2 2 13 cmpo class x ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁡ v + y ⁡ v
15 0 14 wceq wff + r = x ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁡ v + y ⁡ v