![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > sheli | Structured version Visualization version GIF version |
Description: A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
shssi.1 | ⊢ 𝐻 ∈ Sℋ |
Ref | Expression |
---|---|
sheli | ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shssi.1 | . . 3 ⊢ 𝐻 ∈ Sℋ | |
2 | 1 | shssii 30053 | . 2 ⊢ 𝐻 ⊆ ℋ |
3 | 2 | sseli 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 |