Theorem cheli 31524

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

Syntax hints:   → wi 4   ∈ wcel 2149   ℋchba 31211   C_ℋ cch 31221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-hilex 31291

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fv 6545  df-ov 7414  df-sh 31499  df-ch 31513

This theorem is referenced by:  pjhthlem1  31683  pjhthlem2  31684  h1de2ci  31848  spanunsni  31871  spansncvi  31944  3oalem1  31954  pjcompi  31964  pjocini  31990  pjjsi  31992  pjrni  31994  pjdsi  32004  pjds3i  32005  mayete3i  32020  riesz3i  32354  pjnmopi  32440  pjnormssi  32460  pjimai  32468  pjclem4a  32490  pjclem4  32491  pj3lem1  32498  pj3si  32499  strlem1  32542  strlem3  32545  strlem5  32547  hstrlem3  32553  hstrlem5  32555  sumdmdii  32707  sumdmdlem  32710  sumdmdlem2  32711