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

Definition df-hvsub 21512
Description: Define vector subtraction. See hvsubvali 21561 for its value and hvsubcli 21562 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 21466 . 2  class  -h
2 vx . . 3  set  x
3 vy . . 3  set  y
4 chil 21460 . . 3  class  ~H
52cv 1618 . . . 4  class  x
6 c1 8706 . . . . . 6  class  1
76cneg 9006 . . . . 5  class  -u 1
83cv 1618 . . . . 5  class  y
9 csm 21462 . . . . 5  class  .h
107, 8, 9co 5792 . . . 4  class  ( -u
1  .h  y )
11 cva 21461 . . . 4  class  +h
125, 10, 11co 5792 . . 3  class  ( x  +h  ( -u 1  .h  y ) )
132, 3, 4, 4, 12cmpt2 5794 . 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  21518  hvsubf  21556  hvsubval  21557
  Copyright terms: Public domain W3C validator