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

Theorem sheli 30054
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 30053 . 2 𝐻 ⊆ ℋ
32sseli 3939 1 (𝐴𝐻𝐴 ∈ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  chba 29759   S csh 29768
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5255  ax-hilex 29839
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-sh 30047
This theorem is referenced by:  norm1exi  30090  hhssabloi  30102  hhssnv  30104  shscli  30157  shunssi  30208  shmodsi  30229  omlsii  30243  5oalem1  30494  5oalem2  30495  5oalem3  30496  5oalem5  30498  imaelshi  30898  pjimai  31016  shatomici  31198  shatomistici  31201  cdjreui  31272  cdj1i  31273  cdj3lem1  31274  cdj3lem2b  31277  cdj3lem3  31278  cdj3lem3b  31280  cdj3i  31281
  Copyright terms: Public domain W3C validator