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

Definition df-h0v 21566
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 21763. (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 21520 . 2  class  0h
2 cva 21516 . . . . 5  class  +h
3 csm 21517 . . . . 5  class  .h
42, 3cop 3656 . . . 4  class  <.  +h  ,  .h  >.
5 cno 21519 . . . 4  class  normh
64, 5cop 3656 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cn0v 21160 . . 3  class  0vec
86, 7cfv 5271 . 2  class  ( 0vec `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1632 1  wff  0h  =  ( 0vec `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhv0cl-zf  21581  axhvaddid-zf  21582  axhvmul0-zf  21588  axhis4-zf  21593
  Copyright terms: Public domain W3C validator