Definition df-hvsub 27828

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

Assertion

Ref	Expression
df-hvsub	|- -h = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-hvsub

Step	Hyp	Ref	Expression
1		cmv 27782	. 2 class -h
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		chil 27776	. . 3 class ~H
5	2	cv 1482	. . . 4 class x
6		c1 9937	. . . . . 6 class 1
7	6	cneg 10267	. . . . 5 class -u 1
8	3	cv 1482	. . . . 5 class y
9		csm 27778	. . . . 5 class .h
10	7, 8, 9	co 6650	. . . 4 class ( -u 1 .h y )
11		cva 27777	. . . 4 class +h
12	5, 10, 11	co 6650	. . 3 class ( x +h ( -u 1 .h y ) )
13	2, 3, 4, 4, 12	cmpt2 6652	. 2 class ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )
14	1, 13	wceq 1483	1 wff -h = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )

This definition is referenced by:  h2hvs  27834  hvsubf  27872  hvsubval  27873