Metamath Proof Explorer

Theorem ch0

Description: The zero vector belongs to any closed subspace of a Hilbert space. (Contributed by NM, 24-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion ch0 H C 0 H


Step Hyp Ref Expression
1 chsh H C H S
2 sh0 H S 0 H
3 1 2 syl H C 0 H