Theorem cheli 31321

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

Syntax hints:   → wi 4   ∈ wcel 2114   ℋchba 31008   C_ℋ cch 31018

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-hilex 31088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fv 6501  df-ov 7364  df-sh 31296  df-ch 31310

This theorem is referenced by:  pjhthlem1  31480  pjhthlem2  31481  h1de2ci  31645  spanunsni  31668  spansncvi  31741  3oalem1  31751  pjcompi  31761  pjocini  31787  pjjsi  31789  pjrni  31791  pjdsi  31801  pjds3i  31802  mayete3i  31817  riesz3i  32151  pjnmopi  32237  pjnormssi  32257  pjimai  32265  pjclem4a  32287  pjclem4  32288  pj3lem1  32295  pj3si  32296  strlem1  32339  strlem3  32342  strlem5  32344  hstrlem3  32350  hstrlem5  32352  sumdmdii  32504  sumdmdlem  32507  sumdmdlem2  32508