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

Theorem sh0 22568
Description: The zero vector belongs to any subspace of a Hilbert space. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
sh0  |-  ( H  e.  SH  ->  0h  e.  H )

Proof of Theorem sh0
StepHypRef Expression
1 issh 22560 . . 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 ) )
32simprd 450 1  |-  ( H  e.  SH  ->  0h  e.  H )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1717    C_ wss 3265    X. cxp 4818   "cima 4823   CCcc 8923   ~Hchil 22272    +h cva 22273    .h csm 22274   0hc0v 22277   SHcsh 22281
This theorem is referenced by:  ch0  22581  hhssabloi  22612  hhssnv  22614  oc0  22642  ocin  22648  shscli  22669  shsel1  22673  shintcli  22681  shunssi  22720  omlsii  22755  sh0le  22792  imaelshi  23411  shatomistici  23714
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-hilex 22352
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 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-br 4156  df-opab 4210  df-xp 4826  df-cnv 4828  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-sh 22559
  Copyright terms: Public domain W3C validator