Definition df-h0v 30914

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 31112. (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 30868	. 2 class 0ℎ
2		cva 30864	. . . . 5 class +ℎ
3		csm 30865	. . . . 5 class ·ℎ
4	2, 3	cop 4583	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30867	. . . 4 class normℎ
6	4, 5	cop 4583	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 30532	. . 3 class 0vec
8	6, 7	cfv 6482	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhv0cl-zf  30929  axhvaddid-zf  30930  axhvmul0-zf  30936  axhis4-zf  30941