Theorem hl0cl

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

	Ref	Expression
Hypotheses	hl0cl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	hl0cl.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
Assertion	hl0cl	⊢ ( 𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		hl0cl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		hl0cl.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		hlnv	⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec )
4	1 2	nvzcl	⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 )
5	3 4	syl	⊢ ( 𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋 )