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

Theorem chshii 28996
 Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
Hypothesis
Ref Expression
chshi.1 𝐻C
Assertion
Ref Expression
chshii 𝐻S

Proof of Theorem chshii
StepHypRef Expression
1 chshi.1 . 2 𝐻C
2 chsh 28993 . 2 (𝐻C𝐻S )
31, 2ax-mp 5 1 𝐻S
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2107   Sℋ csh 28697   Cℋ cch 28698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fv 6356  df-ov 7151  df-ch 28990 This theorem is referenced by:  chssii  29000  helsh  29014  h0elsh  29025  hhsscms  29047  hhssbnOLD  29048  chocunii  29070  shsleji  29139  shjshcli  29145  pjhthlem1  29160  pjhthlem2  29161  omlsii  29172  ococi  29174  pjoc1i  29200  chne0i  29222  chocini  29223  chjcli  29226  chsleji  29227  chseli  29228  chunssji  29236  chjcomi  29237  chub1i  29238  chlubi  29240  chlej1i  29242  chlej2i  29243  h1de2bi  29323  h1de2ctlem  29324  spansnpji  29347  spanunsni  29348  h1datomi  29350  pjoml2i  29354  qlaxr3i  29405  osumi  29411  osumcor2i  29413  spansnji  29415  spansnm0i  29419  nonbooli  29420  spansncvi  29421  5oai  29430  3oalem2  29432  3oalem5  29435  3oalem6  29436  pjaddii  29444  pjmulii  29446  pjss2i  29449  pjssmii  29450  pj0i  29462  pjocini  29467  pjjsi  29469  pjpythi  29491  mayete3i  29497  pjnmopi  29917  pjimai  29945  pjclem4  29968  pj3si  29976  sto1i  30005  stlei  30009  strlem1  30019  hatomici  30128  hatomistici  30131  atomli  30151  chirredlem3  30161  sumdmdii  30184  sumdmdlem  30187  sumdmdlem2  30188
 Copyright terms: Public domain W3C validator