Theorem cheli 29015

Description: A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.)

Hypothesis

Ref	Expression
chssi.1	⊢ 𝐻 ∈ Cℋ

Assertion

Ref	Expression
cheli	⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Proof of Theorem cheli

Step	Hyp	Ref	Expression
1		chssi.1	. . 3 ⊢ 𝐻 ∈ Cℋ
2	1	chssii 29014	. 2 ⊢ 𝐻 ⊆ ℋ
3	2	sseli 3911	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2111   ℋchba 28702   C_ℋ cch 28712

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-uni 4801  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-iota 6283  df-fv 6332  df-ov 7138  df-sh 28990  df-ch 29004

This theorem is referenced by:  pjhthlem1  29174  pjhthlem2  29175  h1de2ci  29339  spanunsni  29362  spansncvi  29435  3oalem1  29445  pjcompi  29455  pjocini  29481  pjjsi  29483  pjrni  29485  pjdsi  29495  pjds3i  29496  mayete3i  29511  riesz3i  29845  pjnmopi  29931  pjnormssi  29951  pjimai  29959  pjclem4a  29981  pjclem4  29982  pj3lem1  29989  pj3si  29990  strlem1  30033  strlem3  30036  strlem5  30038  hstrlem3  30044  hstrlem5  30046  sumdmdii  30198  sumdmdlem  30201  sumdmdlem2  30202