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

Definition df-hvsub 21381
Description: Define vector subtraction. See hvsubvali 21430 for its value and hvsubcli 21431 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 21335 . 2  class  -h
2 vx . . 3  set  x
3 vy . . 3  set  y
4 chil 21329 . . 3  class  ~H
52cv 1618 . . . 4  class  x
6 c1 8618 . . . . . 6  class  1
76cneg 8918 . . . . 5  class  -u 1
83cv 1618 . . . . 5  class  y
9 csm 21331 . . . . 5  class  .h
107, 8, 9co 5710 . . . 4  class  ( -u
1  .h  y )
11 cva 21330 . . . 4  class  +h
125, 10, 11co 5710 . . 3  class  ( x  +h  ( -u 1  .h  y ) )
132, 3, 4, 4, 12cmpt2 5712 . 2  class  ( x  e.  ~H ,  y  e.  ~H  |->  ( x  +h  ( -u 1  .h  y ) ) )
141, 13wceq 1619 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  21387  hvsubf  21425  hvsubval  21426
  Copyright terms: Public domain W3C validator