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 e. CH -> 0h e. H )

Proof

Step Hyp Ref Expression
1 chsh 
 |-  ( H e. CH -> H e. SH )
2 sh0 
 |-  ( H e. SH -> 0h e. H )
3 1 2 syl 
 |-  ( H e. CH -> 0h e. H )