Definition df-h0v 27827

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 28025. (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 27781	. 2 class 0ℎ
2		cva 27777	. . . . 5 class +ℎ
3		csm 27778	. . . . 5 class ·ℎ
4	2, 3	cop 4183	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 27780	. . . 4 class normℎ
6	4, 5	cop 4183	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 27443	. . 3 class 0vec
8	6, 7	cfv 5888	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1483	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhv0cl-zf  27842  axhvaddid-zf  27843  axhvmul0-zf  27849  axhis4-zf  27854