Definition df-hvsub 31573

Description: Define vector subtraction. See hvsubvali 31622 for its value and hvsubcli 31623 for its closure. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-hvsub	⊢ −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ ( -1 ·ℎ 𝑦)))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-hvsub

Step	Hyp	Ref	Expression
1		cmv 31527	. 2 class −ℎ
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		chba 31521	. . 3 class ℋ
5	2	cv 1569	. . . 4 class 𝑥
6		c1 11201	. . . . . 6 class 1
7	6	cneg 11542	. . . . 5 class -1
8	3	cv 1569	. . . . 5 class 𝑦
9		csm 31523	. . . . 5 class ·ℎ
10	7, 8, 9	co 7420	. . . 4 class ( -1 ·ℎ 𝑦)
11		cva 31522	. . . 4 class +ℎ
12	5, 10, 11	co 7420	. . 3 class (𝑥 +ℎ ( -1 ·ℎ 𝑦))
13	2, 3, 4, 4, 12	cmpo 7422	. 2 class (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ ( -1 ·ℎ 𝑦)))
14	1, 13	wceq 1570	1 wff −ℎ = (𝑥 ∈ ℋ, 𝑦 ∈ ℋ ↦ (𝑥 +ℎ ( -1 ·ℎ 𝑦)))

This definition is used by:  h2hvs  31579  hvsubf  31617  hvsubval  31618