This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐻 ∈ Cℋ → 0ℎ ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 chsh ⊢ ( 𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
2 sh0 ⊢ ( 𝐻 ∈ Sℋ → 0ℎ ∈ 𝐻 )
3 1 2 syl ⊢ ( 𝐻 ∈ Cℋ → 0ℎ ∈ 𝐻 )