Theorem hl0cl

Description: The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hl0cl.1	|- X = ( BaseSet ` U )
	hl0cl.5	|- Z = ( 0vec ` U )
Assertion	hl0cl	|- ( U e. CHilOLD -> Z e. X )

Proof

Step	Hyp	Ref	Expression
1		hl0cl.1	|- X = ( BaseSet ` U )
2		hl0cl.5	|- Z = ( 0vec ` U )
3		hlnv	|- ( U e. CHilOLD -> U e. NrmCVec )
4	1 2	nvzcl	|- ( U e. NrmCVec -> Z e. X )
5	3 4	syl	|- ( U e. CHilOLD -> Z e. X )