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_{\mathrm{vec}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0v	$$class{0}_{ℎ}$$
1		cn0v	$$class{0}_{\mathrm{vec}}$$
2		cva	$$class{+}_{ℎ}$$
3		csm	$$class{\cdot }_{ℎ}$$
4	2 3	cop	$$class⟨{+}_{ℎ},{\cdot }_{ℎ}⟩$$
5		cno	$$class{norm}_{ℎ}$$
6	4 5	cop	$$class⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
7	6 1	cfv	$$class{0}_{\mathrm{vec}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
8	0 7	wceq	$$wff{0}_{ℎ}=0_{\mathrm{vec}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$