Definition df-h0v 28753

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 28951. (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 28707	. 2 class 0ℎ
2		cva 28703	. . . . 5 class +ℎ
3		csm 28704	. . . . 5 class ·ℎ
4	2, 3	cop 4531	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 28706	. . . 4 class normℎ
6	4, 5	cop 4531	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 28371	. . 3 class 0vec
8	6, 7	cfv 6324	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1538	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhv0cl-zf  28768  axhvaddid-zf  28769  axhvmul0-zf  28775  axhis4-zf  28780