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 = ( 0vec ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0v 0
1 cn0v 0vec
2 cva +
3 csm ·
4 2 3 cop ⟨ + , ·
5 cno norm
6 4 5 cop ⟨ ⟨ + , · ⟩ , norm
7 6 1 cfv ( 0vec ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
8 0 7 wceq 0 = ( 0vec ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )