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

Theorem chshii 22730
Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
Hypothesis
Ref Expression
chshi.1  |-  H  e. 
CH
Assertion
Ref Expression
chshii  |-  H  e.  SH

Proof of Theorem chshii
StepHypRef Expression
1 chshi.1 . 2  |-  H  e. 
CH
2 chsh 22727 . 2  |-  ( H  e.  CH  ->  H  e.  SH )
31, 2ax-mp 8 1  |-  H  e.  SH
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   SHcsh 22431   CHcch 22432
This theorem is referenced by:  chssii  22734  helsh  22747  h0elsh  22758  hhsscms  22779  hhssbn  22780  hhsshl  22781  chocunii  22803  shsleji  22872  shjshcli  22878  pjhthlem1  22893  pjhthlem2  22894  omlsii  22905  ococi  22907  pjoc1i  22933  chne0i  22955  chocini  22956  chjcli  22959  chsleji  22960  chseli  22961  chunssji  22969  chjcomi  22970  chub1i  22971  chlubi  22973  chlej1i  22975  chlej2i  22976  h1de2bi  23056  h1de2ctlem  23057  spansnpji  23080  spanunsni  23081  h1datomi  23083  pjoml2i  23087  qlaxr3i  23138  osumi  23144  osumcor2i  23146  spansnji  23148  spansnm0i  23152  nonbooli  23153  spansncvi  23154  5oai  23163  3oalem2  23165  3oalem5  23168  3oalem6  23169  pjaddii  23177  pjmulii  23179  pjss2i  23182  pjssmii  23183  pj0i  23195  pjocini  23200  pjjsi  23202  pjpythi  23224  mayete3i  23230  mayete3iOLD  23231  pjnmopi  23651  pjimai  23679  pjclem4  23702  pj3si  23710  sto1i  23739  stlei  23743  strlem1  23753  hatomici  23862  hatomistici  23865  atomli  23885  chirredlem3  23895  sumdmdii  23918  sumdmdlem  23921  sumdmdlem2  23922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-xp 4884  df-cnv 4886  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fv 5462  df-ov 6084  df-ch 22724
  Copyright terms: Public domain W3C validator