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