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	|- -h = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmv	|- -h
1		vx	|- x
2		chba	|- ~H
3		vy	|- y
4	1	cv	|- x
5		cva	|- +h
6		c1	|- 1
7	6	cneg	|- -u 1
8		csm	|- .h
9	3	cv	|- y
10	7 9 8	co	|- ( -u 1 .h y )
11	4 10 5	co	|- ( x +h ( -u 1 .h y ) )
12	1 3 2 2 11	cmpo	|- ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )
13	0 12	wceq	|- -h = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )