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

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

Proof of Theorem cheli
StepHypRef Expression
1 chssi.1 . . 3  |-  H  e. 
CH
21chssii 22735 . 2  |-  H  C_  ~H
32sseli 3345 1  |-  ( A  e.  H  ->  A  e.  ~H )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   ~Hchil 22423   CHcch 22433
This theorem is referenced by:  pjhthlem1  22894  pjhthlem2  22895  h1de2ci  23059  spanunsni  23082  spansncvi  23155  3oalem1  23165  pjcompi  23175  pjocini  23201  pjjsi  23203  pjrni  23205  pjdsi  23215  pjds3i  23216  mayete3i  23231  mayete3iOLD  23232  riesz3i  23566  pjnmopi  23652  pjnormssi  23672  pjimai  23680  pjclem4a  23702  pjclem4  23703  pj3lem1  23710  pj3si  23711  strlem1  23754  strlem3  23757  strlem5  23759  hstrlem3  23765  hstrlem5  23767  sumdmdii  23919  sumdmdlem  23922  sumdmdlem2  23923
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 2418  ax-sep 4331  ax-hilex 22503
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 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rex 2712  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-opab 4268  df-xp 4885  df-cnv 4887  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fv 5463  df-ov 6085  df-sh 22710  df-ch 22725
  Copyright terms: Public domain W3C validator