Definition df-hvsub

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

	Ref	Expression
Assertion	df-hvsub	$$⊢{-}_{ℎ}=\left(x\in \mathscr{H},y\in \mathscr{H}⟼x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmv	$$class{-}_{ℎ}$$
1		vx	$$setvarx$$
2		chba	$$class\mathscr{H}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		cva	$$class{+}_{ℎ}$$
6		c1	$$class1$$
7	6	cneg	$$class-1$$
8		csm	$$class{\cdot }_{ℎ}$$
9	3	cv	$$setvary$$
10	7 9 8	co	$$class\left(-1{\cdot }_{ℎ}y\right)$$
11	4 10 5	co	$$class\left(x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$
12	1 3 2 2 11	cmpo	$$class\left(x\in \mathscr{H},y\in \mathscr{H}⟼x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$
13	0 12	wceq	$$wff{-}_{ℎ}=\left(x\in \mathscr{H},y\in \mathscr{H}⟼x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$