This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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} (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0v	$class 0_{ℎ}$
1		cn0v	$class 0_{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_{vec} (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$
8	0 7	wceq	$wff 0_{ℎ} = 0_{vec} (⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩)$