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

Definition df-hvsub 21567
Description: Define vector subtraction. See hvsubvali 21616 for its value and hvsubcli 21617 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 21521 . 2  class  -h
2 vx . . 3  set  x
3 vy . . 3  set  y
4 chil 21515 . . 3  class  ~H
52cv 1631 . . . 4  class  x
6 c1 8754 . . . . . 6  class  1
76cneg 9054 . . . . 5  class  -u 1
83cv 1631 . . . . 5  class  y
9 csm 21517 . . . . 5  class  .h
107, 8, 9co 5874 . . . 4  class  ( -u
1  .h  y )
11 cva 21516 . . . 4  class  +h
125, 10, 11co 5874 . . 3  class  ( x  +h  ( -u 1  .h  y ) )
132, 3, 4, 4, 12cmpt2 5876 . 2  class  ( x  e.  ~H ,  y  e.  ~H  |->  ( x  +h  ( -u 1  .h  y ) ) )
141, 13wceq 1632 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  21573  hvsubf  21611  hvsubval  21612
  Copyright terms: Public domain W3C validator