Metamath Proof Explorer

Definition df-subr

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

Ref Expression
Assertion df-subr ⊢ - r = x ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁡ v − y ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminusr 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 cmin 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