Metamath Proof Explorer

Theorem sh0

Description: The zero vector belongs to any subspace of a Hilbert space. (Contributed by NM, 11-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sh0 H S 0 H


Step Hyp Ref Expression
1 issh H S H 0 H + H × H H × H H
2 1 simplbi H S H 0 H
3 2 simprd H S 0 H