Theorem shss 31139

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.)

Assertion

Ref	Expression
shss	⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ)

Proof of Theorem shss

Step	Hyp	Ref	Expression
1		issh 31137	. . 3 ⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻)))
2	1	simplbi 497	. 2 ⊢ (𝐻 ∈ Sℋ → (𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻))
3	2	simpld 494	1 ⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3914   × cxp 5636   “ cima 5641  ℂcc 11066   ℋchba 30848   +_ℎ cva 30849   ·_ℎ csm 30850  0_ℎc0v 30853   S_ℋ csh 30857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-hilex 30928

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-sh 31136

This theorem is referenced by:  shel  31140  shex  31141  shssii  31142  shsubcl  31149  chss  31158  shsspwh  31175  hhsssh  31198  shocel  31211  shocsh  31213  ocss  31214  shocss  31215  shocorth  31221  shococss  31223  shorth  31224  shoccl  31234  shsel  31243  shintcli  31258  spanid  31276  shjval  31280  shjcl  31285  shlej1  31289  shlub  31343  chscllem2  31567  chscllem4  31569