Definition df-h0v

Description: Define the zero vector of Hilbert space. Note that 0vec 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 . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-h0v	⊢ 0ℎ = ( 0vec ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0v	⊢ 0ℎ
1		cn0v	⊢ 0vec
2		cva	⊢ +ℎ
3		csm	⊢ ·ℎ
4	2 3	cop	⊢ ⟨ +ℎ , ·ℎ ⟩
5		cno	⊢ normℎ
6	4 5	cop	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
7	6 1	cfv	⊢ ( 0vec ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
8	0 7	wceq	⊢ 0ℎ = ( 0vec ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )