Theorem cheli 31584

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 31583	. 2 ⊢ 𝐻 ⊆ ℋ
3	2	sseli 3933	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2143   ℋchba 31271   C_ℋ cch 31281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-hilex 31351

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fv 6544  df-ov 7413  df-sh 31559  df-ch 31573

This theorem is referenced by:  pjhthlem1  31743  pjhthlem2  31744  h1de2ci  31908  spanunsni  31931  spansncvi  32004  3oalem1  32014  pjcompi  32024  pjocini  32050  pjjsi  32052  pjrni  32054  pjdsi  32064  pjds3i  32065  mayete3i  32080  riesz3i  32414  pjnmopi  32500  pjnormssi  32520  pjimai  32528  pjclem4a  32550  pjclem4  32551  pj3lem1  32558  pj3si  32559  strlem1  32602  strlem3  32605  strlem5  32607  hstrlem3  32613  hstrlem5  32615  sumdmdii  32767  sumdmdlem  32770  sumdmdlem2  32771