Definition df-h0v 29332

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 29530. (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 29286	. 2 class 0ℎ
2		cva 29282	. . . . 5 class +ℎ
3		csm 29283	. . . . 5 class ·ℎ
4	2, 3	cop 4567	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 29285	. . . 4 class normℎ
6	4, 5	cop 4567	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 28950	. . 3 class 0vec
8	6, 7	cfv 6433	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1539	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhv0cl-zf  29347  axhvaddid-zf  29348  axhvmul0-zf  29354  axhis4-zf  29359