Definition df-h0v 31060

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 31258. (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 31014	. 2 class 0ℎ
2		cva 31010	. . . . 5 class +ℎ
3		csm 31011	. . . . 5 class ·ℎ
4	2, 3	cop 4562	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31013	. . . 4 class normℎ
6	4, 5	cop 4562	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 30678	. . 3 class 0vec
8	6, 7	cfv 6486	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1547	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhv0cl-zf  31075  axhvaddid-zf  31076  axhvmul0-zf  31082  axhis4-zf  31087