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

Theorem chssii 28397
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 28393 . 2 𝐻S
32shssii 28379 1 𝐻 ⊆ ℋ
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  wss 3715  chil 28085   C cch 28095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-hilex 28165
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-xp 5272  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fv 6057  df-ov 6816  df-sh 28373  df-ch 28387
This theorem is referenced by:  cheli  28398  chelii  28399  hhsscms  28445  chocvali  28467  chm1i  28624  chsscon3i  28629  chsscon2i  28631  chjoi  28656  chj1i  28657  shjshsi  28660  sshhococi  28714  h1dei  28718  spansnpji  28746  spanunsni  28747  h1datomi  28749  spansnji  28814  pjfi  28872  riesz3i  29230  hmopidmpji  29320  pjoccoi  29346  pjinvari  29359  stcltr2i  29443  mdsymi  29579  mdcompli  29597  dmdcompli  29598
  Copyright terms: Public domain W3C validator