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

Theorem shss 26724
Description: A subspace is a subset of Hilbert space. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
shss  |-  ( H  e.  SH  ->  H  C_ 
~H )

Proof of Theorem shss
StepHypRef Expression
1 issh 26722 . . 3  |-  ( H  e.  SH  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  (
(  +h  " ( H  X.  H ) ) 
C_  H  /\  (  .h  " ( CC  X.  H ) )  C_  H ) ) )
21simplbi 461 . 2  |-  ( H  e.  SH  ->  ( H  C_  ~H  /\  0h  e.  H ) )
32simpld 460 1  |-  ( H  e.  SH  ->  H  C_ 
~H )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1867    C_ wss 3433    X. cxp 4843   "cima 4848   CCcc 9526   ~Hchil 26433    +h cva 26434    .h csm 26435   0hc0v 26438   SHcsh 26442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-hilex 26513
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-xp 4851  df-cnv 4853  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-sh 26721
This theorem is referenced by:  shel  26725  shex  26726  shssii  26727  shsubcl  26734  chss  26743  shsspwh  26760  hhsssh  26781  shocel  26796  shocsh  26798  ocss  26799  shocss  26800  shocorth  26806  shococss  26808  shorth  26809  shoccl  26819  shsel  26828  shintcli  26843  spanid  26861  shjval  26865  shjcl  26870  shlej1  26874  shlub  26928  chscllem2  27152  chscllem4  27154
  Copyright terms: Public domain W3C validator