![]() |
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 28996 | . 2 ⊢ 𝐻 ⊆ ℋ |
3 | 2 | sseli 3911 | 1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 ℋchba 28702 Sℋ csh 28711 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-hilex 28782 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-rab 3115 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-xp 5525 df-cnv 5527 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-sh 28990 |
This theorem is referenced by: norm1exi 29033 hhssabloi 29045 hhssnv 29047 shscli 29100 shunssi 29151 shmodsi 29172 omlsii 29186 5oalem1 29437 5oalem2 29438 5oalem3 29439 5oalem5 29441 imaelshi 29841 pjimai 29959 shatomici 30141 shatomistici 30144 cdjreui 30215 cdj1i 30216 cdj3lem1 30217 cdj3lem2b 30220 cdj3lem3 30221 cdj3lem3b 30223 cdj3i 30224 |
Copyright terms: Public domain | W3C validator |