![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > cheli | Structured version Visualization version GIF version |
Description: A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
chssi.1 | ⊢ 𝐻 ∈ Cℋ |
Ref | Expression |
---|---|
cheli | ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chssi.1 | . . 3 ⊢ 𝐻 ∈ Cℋ | |
2 | 1 | chssii 28216 | . 2 ⊢ 𝐻 ⊆ ℋ |
3 | 2 | sseli 3632 | 1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 ℋchil 27904 Cℋ cch 27914 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-hilex 27984 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-opab 4746 df-xp 5149 df-cnv 5151 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-iota 5889 df-fv 5934 df-ov 6693 df-sh 28192 df-ch 28206 |
This theorem is referenced by: pjhthlem1 28378 pjhthlem2 28379 h1de2ci 28543 spanunsni 28566 spansncvi 28639 3oalem1 28649 pjcompi 28659 pjocini 28685 pjjsi 28687 pjrni 28689 pjdsi 28699 pjds3i 28700 mayete3i 28715 riesz3i 29049 pjnmopi 29135 pjnormssi 29155 pjimai 29163 pjclem4a 29185 pjclem4 29186 pj3lem1 29193 pj3si 29194 strlem1 29237 strlem3 29240 strlem5 29242 hstrlem3 29248 hstrlem5 29250 sumdmdii 29402 sumdmdlem 29405 sumdmdlem2 29406 |
Copyright terms: Public domain | W3C validator |