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

Theorem chssii 29014
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
chssi.1 𝐻C
Assertion
Ref Expression
chssii 𝐻 ⊆ ℋ

Proof of Theorem chssii
StepHypRef Expression
1 chssi.1 . . 3 𝐻C
21chshii 29010 . 2 𝐻S
32shssii 28996 1 𝐻 ⊆ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  wss 3881  chba 28702   C cch 28712
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 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-hilex 28782
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 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fv 6332  df-ov 7138  df-sh 28990  df-ch 29004
This theorem is referenced by:  cheli  29015  chelii  29016  hhsscms  29061  chocvali  29082  chm1i  29239  chsscon3i  29244  chsscon2i  29246  chjoi  29271  chj1i  29272  shjshsi  29275  sshhococi  29329  h1dei  29333  spansnpji  29361  spanunsni  29362  h1datomi  29364  spansnji  29429  pjfi  29487  riesz3i  29845  hmopidmpji  29935  pjoccoi  29961  pjinvari  29974  stcltr2i  30058  mdsymi  30194  mdcompli  30212  dmdcompli  30213
  Copyright terms: Public domain W3C validator