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

Theorem chssii 24771
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  |-  H  e. 
CH
Assertion
Ref Expression
chssii  |-  H  C_  ~H

Proof of Theorem chssii
StepHypRef Expression
1 chssi.1 . . 3  |-  H  e. 
CH
21chshii 24767 . 2  |-  H  e.  SH
32shssii 24752 1  |-  H  C_  ~H
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758    C_ wss 3428   ~Hchil 24458   CHcch 24468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-hilex 24538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-pw 3962  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-opab 4451  df-xp 4946  df-cnv 4948  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5481  df-fv 5526  df-ov 6195  df-sh 24746  df-ch 24761
This theorem is referenced by:  cheli  24772  chelii  24773  hhsscms  24817  chocvali  24839  chm1i  24996  chsscon3i  25001  chsscon2i  25003  chjoi  25028  chj1i  25029  shjshsi  25032  sshhococi  25086  h1dei  25090  spansnpji  25118  spanunsni  25119  h1datomi  25121  spansnji  25186  pjfi  25244  riesz3i  25603  hmopidmpji  25693  pjoccoi  25719  pjinvari  25732  stcltr2i  25816  mdsymi  25952  mdcompli  25970  dmdcompli  25971
  Copyright terms: Public domain W3C validator