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

Theorem chsh 27930
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 27928 . 2 (𝐻C ↔ (𝐻S ∧ ( ⇝𝑣 “ (𝐻𝑚 ℕ)) ⊆ 𝐻))
21simplbi 476 1 (𝐻C𝐻S )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wss 3555  cima 5077  (class class class)co 6604  𝑚 cmap 7802  cn 10964  𝑣 chli 27633   S csh 27634   C cch 27635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-xp 5080  df-cnv 5082  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fv 5855  df-ov 6607  df-ch 27927
This theorem is referenced by:  chsssh  27931  chshii  27933  ch0  27934  chss  27935  choccl  28014  chjval  28060  chjcl  28065  pjhth  28101  pjhtheu  28102  pjpreeq  28106  pjpjpre  28127  ch0le  28149  chle0  28151  chslej  28206  chjcom  28214  chub1  28215  chlub  28217  chlej1  28218  chlej2  28219  spansnsh  28269  fh1  28326  fh2  28327  chscllem1  28345  chscllem2  28346  chscllem3  28347  chscllem4  28348  chscl  28349  pjorthi  28377  pjoi0  28425  hstoc  28930  hstnmoc  28931  ch1dle  29060  atomli  29090  chirredlem3  29100  sumdmdii  29123
  Copyright terms: Public domain W3C validator