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

Theorem chsh 26436
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 26434 . 2  |-  ( H  e.  CH  <->  ( H  e.  SH  /\  (  ~~>v  "
( H  ^m  NN ) )  C_  H
) )
21simplbi 458 1  |-  ( H  e.  CH  ->  H  e.  SH )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842    C_ wss 3413   "cima 4945  (class class class)co 6234    ^m cmap 7377   NNcn 10496    ~~>v chli 26138   SHcsh 26139   CHcch 26140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-xp 4948  df-cnv 4950  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-iota 5489  df-fv 5533  df-ov 6237  df-ch 26433
This theorem is referenced by:  chsssh  26437  chshii  26439  ch0  26440  chss  26441  choccl  26518  chjval  26564  chjcl  26569  pjhth  26605  pjhtheu  26606  pjpreeq  26610  pjpjpre  26631  ch0le  26653  chle0  26655  chslej  26710  chjcom  26718  chub1  26719  chlub  26721  chlej1  26722  chlej2  26723  spansnsh  26773  fh1  26830  fh2  26831  chscllem1  26849  chscllem2  26850  chscllem3  26851  chscllem4  26852  chscl  26853  pjorthi  26881  pjoi0  26929  hstoc  27434  hstnmoc  27435  ch1dle  27564  atomli  27594  chirredlem3  27604  sumdmdii  27627
  Copyright terms: Public domain W3C validator