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	|- 0h = ( 0vec ` <. <. +h , .h >. , normh >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0v	|- 0h
1		cn0v	|- 0vec
2		cva	|- +h
3		csm	|- .h
4	2 3	cop	|- <. +h , .h >.
5		cno	|- normh
6	4 5	cop	|- <. <. +h , .h >. , normh >.
7	6 1	cfv	|- ( 0vec ` <. <. +h , .h >. , normh >. )
8	0 7	wceq	|- 0h = ( 0vec ` <. <. +h , .h >. , normh >. )