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 0 = 0 vec + norm

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0v class 0
1 cn0v class 0 vec
2 cva class +
3 csm class
4 2 3 cop class +
5 cno class norm
6 4 5 cop class + norm
7 6 1 cfv class 0 vec + norm
8 0 7 wceq wff 0 = 0 vec + norm