HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  shssii Structured version   Visualization version   GIF version

Theorem shssii 28994
Description: A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
Hypothesis
Ref Expression
shssi.1 𝐻S
Assertion
Ref Expression
shssii 𝐻 ⊆ ℋ

Proof of Theorem shssii
StepHypRef Expression
1 shssi.1 . 2 𝐻S
2 shss 28991 . 2 (𝐻S𝐻 ⊆ ℋ)
31, 2ax-mp 5 1 𝐻 ⊆ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  wss 3908  chba 28700   S csh 28709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-hilex 28780
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-br 5043  df-opab 5105  df-xp 5538  df-cnv 5540  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-sh 28988
This theorem is referenced by:  sheli  28995  shelii  28996  chssii  29012  hhssabloilem  29042  hhssabloi  29043  hhssnv  29045  hhssba  29052  shunssji  29150  shsval3i  29169  shjshsi  29273  span0  29323  spanuni  29325  imaelshi  29839  nlelchi  29842  hmopidmchi  29932  pjimai  29957  shatomistici  30142
  Copyright terms: Public domain W3C validator