Definition df-h0v 30950

Description: Define the zero vector of Hilbert space. Note that 0_vec 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 31148. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-h0v	⊢ 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

Detailed syntax breakdown of Definition df-h0v

Step	Hyp	Ref	Expression
1		c0v 30904	. 2 class 0ℎ
2		cva 30900	. . . . 5 class +ℎ
3		csm 30901	. . . . 5 class ·ℎ
4	2, 3	cop 4579	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30903	. . . 4 class normℎ
6	4, 5	cop 4579	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 30568	. . 3 class 0vec
8	6, 7	cfv 6481	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1541	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhv0cl-zf  30965  axhvaddid-zf  30966  axhvmul0-zf  30972  axhis4-zf  30977