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

Theorem sheli 28905
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 𝐻S
Assertion
Ref Expression
sheli (𝐴𝐻𝐴 ∈ ℋ)

Proof of Theorem sheli
StepHypRef Expression
1 shssi.1 . . 3 𝐻S
21shssii 28904 . 2 𝐻 ⊆ ℋ
32sseli 3967 1 (𝐴𝐻𝐴 ∈ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  chba 28610   S csh 28619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-hilex 28690
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-xp 5560  df-cnv 5562  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-sh 28898
This theorem is referenced by:  norm1exi  28941  hhssabloi  28953  hhssnv  28955  shscli  29008  shunssi  29059  shmodsi  29080  omlsii  29094  5oalem1  29345  5oalem2  29346  5oalem3  29347  5oalem5  29349  imaelshi  29749  pjimai  29867  shatomici  30049  shatomistici  30052  cdjreui  30123  cdj1i  30124  cdj3lem1  30125  cdj3lem2b  30128  cdj3lem3  30129  cdj3lem3b  30131  cdj3i  30132
  Copyright terms: Public domain W3C validator