Metamath Proof Explorer


Theorem shss

Description: A subspace is a subset of Hilbert space. (Contributed by NM, 9-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion shss ( 𝐻S𝐻 ⊆ ℋ )

Proof

Step Hyp Ref Expression
1 issh ( 𝐻S ↔ ( ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) ∧ ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )
2 1 simplbi ( 𝐻S → ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) )
3 2 simpld ( 𝐻S𝐻 ⊆ ℋ )