HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hvsub Structured version   Unicode version

Definition df-hvsub 22475
Description: Define vector subtraction. See hvsubvali 22524 for its value and hvsubcli 22525 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
StepHypRef Expression
1 cmv 22429 . 2  class  -h
2 vx . . 3  set  x
3 vy . . 3  set  y
4 chil 22423 . . 3  class  ~H
52cv 1652 . . . 4  class  x
6 c1 8992 . . . . . 6  class  1
76cneg 9293 . . . . 5  class  -u 1
83cv 1652 . . . . 5  class  y
9 csm 22425 . . . . 5  class  .h
107, 8, 9co 6082 . . . 4  class  ( -u
1  .h  y )
11 cva 22424 . . . 4  class  +h
125, 10, 11co 6082 . . 3  class  ( x  +h  ( -u 1  .h  y ) )
132, 3, 4, 4, 12cmpt2 6084 . 2  class  ( x  e.  ~H ,  y  e.  ~H  |->  ( x  +h  ( -u 1  .h  y ) ) )
141, 13wceq 1653 1  wff  -h  =  ( x  e.  ~H ,  y  e.  ~H  |->  ( x  +h  ( -u 1  .h  y ) ) )
Colors of variables: wff set class
This definition is referenced by:  h2hvs  22481  hvsubf  22519  hvsubval  22520
  Copyright terms: Public domain W3C validator