Definition df-hvsub 11468

Description: Define vector subtraction. See hvsubvali 11518 for its value and hvsubcli 11519 for its closure.

Assertion

Ref	Expression
df-hvsub	|- -h = {<.<.x, y>., z>. | ((x e. ~H /\ y e. ~H) /\ z = (x +h (-u1 .h y)))}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-hvsub

Step	Hyp	Ref	Expression
1		cmv 11420	. 2 class -h
2		vx	. . . . . . 7 set x
3	2	cv 1614	. . . . . 6 class x
4		chil 11416	. . . . . 6 class ~H
5	3, 4	wcel 1617	. . . . 5 wff x e. ~H
6		vy	. . . . . . 7 set y
7	6	cv 1614	. . . . . 6 class y
8	7, 4	wcel 1617	. . . . 5 wff y e. ~H
9	5, 8	wa 433	. . . 4 wff (x e. ~H /\ y e. ~H)
10		vz	. . . . . 6 set z
11	10	cv 1614	. . . . 5 class z
12		c1 6830	. . . . . . . 8 class 1
13	12	cneg 7092	. . . . . . 7 class -u1
14		csm 11418	. . . . . . 7 class .h
15	13, 7, 14	co 5020	. . . . . 6 class (-u1 .h y)
16		cva 11417	. . . . . 6 class +h
17	3, 15, 16	co 5020	. . . . 5 class (x +h (-u1 .h y))
18	11, 17	wceq 1615	. . . 4 wff z = (x +h (-u1 .h y))
19	9, 18	wa 433	. . 3 wff ((x e. ~H /\ y e. ~H) /\ z = (x +h (-u1 .h y)))
20	19, 2, 6, 10	copab2 5021	. 2 class {<.<.x, y>., z>. | ((x e. ~H /\ y e. ~H) /\ z = (x +h (-u1 .h y)))}
21	1, 20	wceq 1615	1 wff -h = {<.<.x, y>., z>. | ((x e. ~H /\ y e. ~H) /\ z = (x +h (-u1 .h y)))}

This definition is referenced by:  h2hvs 11474  hvsubopr 11513  hvsubval 11514

Copyright terms: Public domain