Definition df-h0v 31587

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 31785. (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 31541	. 2 class 0ℎ
2		cva 31537	. . . . 5 class +ℎ
3		csm 31538	. . . . 5 class ·ℎ
4	2, 3	cop 4838	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31540	. . . 4 class normℎ
6	4, 5	cop 4838	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 31205	. . 3 class 0vec
8	6, 7	cfv 6547	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1569	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is used by:  axhv0cl-zf  31602  axhvaddid-zf  31603  axhvmul0-zf  31609  axhis4-zf  31614