Definition df-hvsub 4996

Description: Define vector subtraction. See hvsubval 5001 for its value and hvsubcl 5002 for its closure.

Assertion

Ref	Expression
df-hvsub	⊢ −v = {⟨⟨x, y⟩, z⟩∣((x ∈ ℋ ∧ y ∈ ℋ ) ∧ z = (x +v (-1 ·s y)))}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-hvsub

Step	Hyp	Ref	Expression
1		cmv 4962	. 2 class −v
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		chil 4958	. . . . . 6 class ℋ
5	3, 4	wcel 1092	. . . . 5 wff x ∈ ℋ
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ ℋ
9	5, 8	wa 196	. . . 4 wff (x ∈ ℋ ∧ y ∈ ℋ )
10		vz	. . . . . 6 set z
11	10	cv 1089	. . . . 5 class z
12		c1 4029	. . . . . . . 8 class 1
13	12	cneg 4090	. . . . . . 7 class -1
14		csm 4960	. . . . . . 7 class ·s
15	13, 7, 14	co 3001	. . . . . 6 class (-1 ·s y)
16		cva 4959	. . . . . 6 class +v
17	3, 15, 16	co 3001	. . . . 5 class (x +v (-1 ·s y))
18	11, 17	wceq 1091	. . . 4 wff z = (x +v (-1 ·s y))
19	9, 18	wa 196	. . 3 wff ((x ∈ ℋ ∧ y ∈ ℋ ) ∧ z = (x +v (-1 ·s y)))
20	19, 2, 6, 10	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ ℋ ∧ y ∈ ℋ ) ∧ z = (x +v (-1 ·s y)))}
21	1, 20	wceq 1091	1 wff −v = {⟨⟨x, y⟩, z⟩∣((x ∈ ℋ ∧ y ∈ ℋ ) ∧ z = (x +v (-1 ·s y)))}

This definition is referenced by:  hvsubvalt 4997

metamath.org