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

Theorem chsh 22577
Description: A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
chsh  |-  ( H  e.  CH  ->  H  e.  SH )

Proof of Theorem chsh
StepHypRef Expression
1 isch 22575 . 2  |-  ( H  e.  CH  <->  ( H  e.  SH  /\  (  ~~>v  "
( H  ^m  NN ) )  C_  H
) )
21simplbi 447 1  |-  ( H  e.  CH  ->  H  e.  SH )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717    C_ wss 3265   "cima 4823  (class class class)co 6022    ^m cmap 6956   NNcn 9934    ~~>v chli 22280   SHcsh 22281   CHcch 22282
This theorem is referenced by:  chsssh  22578  chshii  22580  ch0  22581  chss  22582  choccl  22658  chjval  22704  chjcl  22709  pjhth  22745  pjhtheu  22746  pjpreeq  22750  pjpjpre  22771  ch0le  22793  chle0  22795  chslej  22850  chjcom  22858  chub1  22859  chlub  22861  chlej1  22862  chlej2  22863  spansnsh  22913  fh1  22970  fh2  22971  chscllem1  22989  chscllem2  22990  chscllem3  22991  chscllem4  22992  chscl  22993  pjorthi  23021  pjoi0  23069  hstoc  23575  hstnmoc  23576  ch1dle  23705  atomli  23735  chirredlem3  23745  sumdmdii  23768
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-xp 4826  df-cnv 4828  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fv 5404  df-ov 6025  df-ch 22574
  Copyright terms: Public domain W3C validator