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

Theorem cheli 28607
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 28606 . 2 𝐻 ⊆ ℋ
32sseli 3793 1 (𝐴𝐻𝐴 ∈ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  chba 28294   C cch 28304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-hilex 28374
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-rex 3094  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4628  df-br 4843  df-opab 4905  df-xp 5317  df-cnv 5319  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6063  df-fv 6108  df-ov 6880  df-sh 28582  df-ch 28596
This theorem is referenced by:  pjhthlem1  28768  pjhthlem2  28769  h1de2ci  28933  spanunsni  28956  spansncvi  29029  3oalem1  29039  pjcompi  29049  pjocini  29075  pjjsi  29077  pjrni  29079  pjdsi  29089  pjds3i  29090  mayete3i  29105  riesz3i  29439  pjnmopi  29525  pjnormssi  29545  pjimai  29553  pjclem4a  29575  pjclem4  29576  pj3lem1  29583  pj3si  29584  strlem1  29627  strlem3  29630  strlem5  29632  hstrlem3  29638  hstrlem5  29640  sumdmdii  29792  sumdmdlem  29795  sumdmdlem2  29796
  Copyright terms: Public domain W3C validator