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

Theorem cheli 28994
 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 𝐻C
Assertion
Ref Expression
cheli (𝐴𝐻𝐴 ∈ ℋ)

Proof of Theorem cheli
StepHypRef Expression
1 chssi.1 . . 3 𝐻C
21chssii 28993 . 2 𝐻 ⊆ ℋ
32sseli 3939 1 (𝐴𝐻𝐴 ∈ ℋ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2115   ℋchba 28681   Cℋ cch 28691 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-hilex 28761 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-xp 5534  df-cnv 5536  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fv 6336  df-ov 7133  df-sh 28969  df-ch 28983 This theorem is referenced by:  pjhthlem1  29153  pjhthlem2  29154  h1de2ci  29318  spanunsni  29341  spansncvi  29414  3oalem1  29424  pjcompi  29434  pjocini  29460  pjjsi  29462  pjrni  29464  pjdsi  29474  pjds3i  29475  mayete3i  29490  riesz3i  29824  pjnmopi  29910  pjnormssi  29930  pjimai  29938  pjclem4a  29960  pjclem4  29961  pj3lem1  29968  pj3si  29969  strlem1  30012  strlem3  30015  strlem5  30017  hstrlem3  30023  hstrlem5  30025  sumdmdii  30177  sumdmdlem  30180  sumdmdlem2  30181
 Copyright terms: Public domain W3C validator