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

Theorem sheli 28402
 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 28401 . 2 𝐻 ⊆ ℋ
32sseli 3741 1 (𝐴𝐻𝐴 ∈ ℋ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2140   ℋchil 28107   Sℋ csh 28116 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-hilex 28187 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806  df-opab 4866  df-xp 5273  df-cnv 5275  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-sh 28395 This theorem is referenced by:  norm1exi  28438  hhssabloi  28450  hhssnv  28452  shscli  28507  shunssi  28558  shmodsi  28579  omlsii  28593  5oalem1  28844  5oalem2  28845  5oalem3  28846  5oalem5  28848  imaelshi  29248  pjimai  29366  shatomici  29548  shatomistici  29551  cdjreui  29622  cdj1i  29623  cdj3lem1  29624  cdj3lem2b  29627  cdj3lem3  29628  cdj3lem3b  29630  cdj3i  29631
 Copyright terms: Public domain W3C validator