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

Theorem chsh 30986
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 (𝐻C𝐻S )

Proof of Theorem chsh
StepHypRef Expression
1 isch 30984 . 2 (𝐻C ↔ (𝐻S ∧ ( ⇝𝑣 “ (𝐻m ℕ)) ⊆ 𝐻))
21simplbi 497 1 (𝐻C𝐻S )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2098  wss 3943  cima 5672  (class class class)co 7405  m cmap 8822  cn 12216  𝑣 chli 30689   S csh 30690   C cch 30691
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-xp 5675  df-cnv 5677  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fv 6545  df-ov 7408  df-ch 30983
This theorem is referenced by:  chsssh  30987  chshii  30989  ch0  30990  chss  30991  choccl  31068  chjval  31114  chjcl  31119  pjhth  31155  pjhtheu  31156  pjpreeq  31160  pjpjpre  31181  ch0le  31203  chle0  31205  chslej  31260  chjcom  31268  chub1  31269  chlub  31271  chlej1  31272  chlej2  31273  spansnsh  31323  fh1  31380  fh2  31381  chscllem1  31399  chscllem2  31400  chscllem3  31401  chscllem4  31402  chscl  31403  pjorthi  31431  pjoi0  31479  hstoc  31984  hstnmoc  31985  ch1dle  32114  atomli  32144  chirredlem3  32154  sumdmdii  32177
  Copyright terms: Public domain W3C validator