Definition df-h0v 31175

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 31373. (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 31129	. 2 class 0ℎ
2		cva 31125	. . . . 5 class +ℎ
3		csm 31126	. . . . 5 class ·ℎ
4	2, 3	cop 4590	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31128	. . . 4 class normℎ
6	4, 5	cop 4590	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cn0v 30793	. . 3 class 0vec
8	6, 7	cfv 6523	. 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1562	1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhv0cl-zf  31190  axhvaddid-zf  31191  axhvmul0-zf  31197  axhis4-zf  31202