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

Theorem shss 22673
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 22671 . . 3  |-  ( H  e.  SH  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  (
(  +h  " ( H  X.  H ) ) 
C_  H  /\  (  .h  " ( CC  X.  H ) )  C_  H ) ) )
21simplbi 447 . 2  |-  ( H  e.  SH  ->  ( H  C_  ~H  /\  0h  e.  H ) )
32simpld 446 1  |-  ( H  e.  SH  ->  H  C_ 
~H )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721    C_ wss 3288    X. cxp 4843   "cima 4848   CCcc 8952   ~Hchil 22383    +h cva 22384    .h csm 22385   0hc0v 22388   SHcsh 22392
This theorem is referenced by:  shel  22674  shex  22675  shssii  22676  shsubcl  22684  chss  22693  shsspwh  22709  hhsssh  22730  shocel  22745  shocsh  22747  ocss  22748  shocss  22749  shocorth  22755  shococss  22757  shorth  22758  shoccl  22768  shsel  22777  shintcli  22792  spanid  22810  shjval  22814  shjcl  22819  shlej1  22823  shlub  22877  chscllem2  23101  chscllem4  23103
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-hilex 22463
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-br 4181  df-opab 4235  df-xp 4851  df-cnv 4853  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-sh 22670
  Copyright terms: Public domain W3C validator