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

Definition df-h0v 22473
Description: Define the zero vector of Hilbert space. Note that  0vec is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as theorem hh0v 22670. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-h0v  |-  0h  =  ( 0vec `  <. <.  +h  ,  .h  >. ,  normh >. )

Detailed syntax breakdown of Definition df-h0v
StepHypRef Expression
1 c0v 22427 . 2  class  0h
2 cva 22423 . . . . 5  class  +h
3 csm 22424 . . . . 5  class  .h
42, 3cop 3817 . . . 4  class  <.  +h  ,  .h  >.
5 cno 22426 . . . 4  class  normh
64, 5cop 3817 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cn0v 22067 . . 3  class  0vec
86, 7cfv 5454 . 2  class  ( 0vec `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1652 1  wff  0h  =  ( 0vec `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhv0cl-zf  22488  axhvaddid-zf  22489  axhvmul0-zf  22495  axhis4-zf  22500
  Copyright terms: Public domain W3C validator