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

Theorem shss 22714
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 22712 . . 3  |-  ( H  e.  SH  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  (
(  +h  " ( H  X.  H ) ) 
C_  H  /\  (  .h  " ( CC  X.  H ) )  C_  H ) ) )
21simplbi 448 . 2  |-  ( H  e.  SH  ->  ( H  C_  ~H  /\  0h  e.  H ) )
32simpld 447 1  |-  ( H  e.  SH  ->  H  C_ 
~H )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726    C_ wss 3322    X. cxp 4878   "cima 4883   CCcc 8990   ~Hchil 22424    +h cva 22425    .h csm 22426   0hc0v 22429   SHcsh 22433
This theorem is referenced by:  shel  22715  shex  22716  shssii  22717  shsubcl  22725  chss  22734  shsspwh  22750  hhsssh  22771  shocel  22786  shocsh  22788  ocss  22789  shocss  22790  shocorth  22796  shococss  22798  shorth  22799  shoccl  22809  shsel  22818  shintcli  22833  spanid  22851  shjval  22855  shjcl  22860  shlej1  22864  shlub  22918  chscllem2  23142  chscllem4  23144
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-hilex 22504
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-br 4215  df-opab 4269  df-xp 4886  df-cnv 4888  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-sh 22711
  Copyright terms: Public domain W3C validator