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

Definition df-h0v 21550
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 21747. (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 21504 . 2  class  0h
2 cva 21500 . . . . 5  class  +h
3 csm 21501 . . . . 5  class  .h
42, 3cop 3643 . . . 4  class  <.  +h  ,  .h  >.
5 cno 21503 . . . 4  class  normh
64, 5cop 3643 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cn0v 21144 . . 3  class  0vec
86, 7cfv 5255 . 2  class  ( 0vec `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1623 1  wff  0h  =  ( 0vec `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhv0cl-zf  21565  axhvaddid-zf  21566  axhvmul0-zf  21572  axhis4-zf  21577
  Copyright terms: Public domain W3C validator