Metamath Proof Explorer


Definition df-h0v

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 . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Assertion df-h0v
|- 0h = ( 0vec ` <. <. +h , .h >. , normh >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0v
 |-  0h
1 cn0v
 |-  0vec
2 cva
 |-  +h
3 csm
 |-  .h
4 2 3 cop
 |-  <. +h , .h >.
5 cno
 |-  normh
6 4 5 cop
 |-  <. <. +h , .h >. , normh >.
7 6 1 cfv
 |-  ( 0vec ` <. <. +h , .h >. , normh >. )
8 0 7 wceq
 |-  0h = ( 0vec ` <. <. +h , .h >. , normh >. )