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

Definition df-hvsub 22512
Description: Define vector subtraction. See hvsubvali 22561 for its value and hvsubcli 22562 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 22466 . 2  class  -h
2 vx . . 3  set  x
3 vy . . 3  set  y
4 chil 22460 . . 3  class  ~H
52cv 1653 . . . 4  class  x
6 c1 9029 . . . . . 6  class  1
76cneg 9330 . . . . 5  class  -u 1
83cv 1653 . . . . 5  class  y
9 csm 22462 . . . . 5  class  .h
107, 8, 9co 6117 . . . 4  class  ( -u
1  .h  y )
11 cva 22461 . . . 4  class  +h
125, 10, 11co 6117 . . 3  class  ( x  +h  ( -u 1  .h  y ) )
132, 3, 4, 4, 12cmpt2 6119 . 2  class  ( x  e.  ~H ,  y  e.  ~H  |->  ( x  +h  ( -u 1  .h  y ) ) )
141, 13wceq 1654 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  22518  hvsubf  22556  hvsubval  22557
  Copyright terms: Public domain W3C validator