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

Theorem sheli 24769
Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)
Hypothesis
Ref Expression
shssi.1  |-  H  e.  SH
Assertion
Ref Expression
sheli  |-  ( A  e.  H  ->  A  e.  ~H )

Proof of Theorem sheli
StepHypRef Expression
1 shssi.1 . . 3  |-  H  e.  SH
21shssii 24768 . 2  |-  H  C_  ~H
32sseli 3461 1  |-  ( A  e.  H  ->  A  e.  ~H )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   ~Hchil 24474   SHcsh 24483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-hilex 24554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402  df-opab 4460  df-xp 4955  df-cnv 4957  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-sh 24762
This theorem is referenced by:  norm1exi  24806  hhssabloi  24816  hhssnv  24818  shscli  24873  shunssi  24924  shmodsi  24945  omlsii  24959  5oalem1  25210  5oalem2  25211  5oalem3  25212  5oalem5  25214  imaelshi  25615  pjimai  25733  shatomici  25915  shatomistici  25918  cdjreui  25989  cdj1i  25990  cdj3lem1  25991  cdj3lem2b  25994  cdj3lem3  25995  cdj3lem3b  25997  cdj3i  25998
  Copyright terms: Public domain W3C validator