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

Theorem chshii 27270
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 27267 . 2 (𝐻C𝐻S )
31, 2ax-mp 5 1 𝐻S
Colors of variables: wff setvar class
Syntax hints:  wcel 1975   S csh 26971   C cch 26972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-xp 5030  df-cnv 5032  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fv 5794  df-ov 6526  df-ch 27264
This theorem is referenced by:  chssii  27274  helsh  27288  h0elsh  27299  hhsscms  27322  hhssbn  27323  hhsshl  27324  chocunii  27346  shsleji  27415  shjshcli  27421  pjhthlem1  27436  pjhthlem2  27437  omlsii  27448  ococi  27450  pjoc1i  27476  chne0i  27498  chocini  27499  chjcli  27502  chsleji  27503  chseli  27504  chunssji  27512  chjcomi  27513  chub1i  27514  chlubi  27516  chlej1i  27518  chlej2i  27519  h1de2bi  27599  h1de2ctlem  27600  spansnpji  27623  spanunsni  27624  h1datomi  27626  pjoml2i  27630  qlaxr3i  27681  osumi  27687  osumcor2i  27689  spansnji  27691  spansnm0i  27695  nonbooli  27696  spansncvi  27697  5oai  27706  3oalem2  27708  3oalem5  27711  3oalem6  27712  pjaddii  27720  pjmulii  27722  pjss2i  27725  pjssmii  27726  pj0i  27738  pjocini  27743  pjjsi  27745  pjpythi  27767  mayete3i  27773  pjnmopi  28193  pjimai  28221  pjclem4  28244  pj3si  28252  sto1i  28281  stlei  28285  strlem1  28295  hatomici  28404  hatomistici  28407  atomli  28427  chirredlem3  28437  sumdmdii  28460  sumdmdlem  28463  sumdmdlem2  28464
  Copyright terms: Public domain W3C validator