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 3911	1 ⊢ (𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2119   ℋ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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-hilex 31088

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fv 6493  df-ov 7359  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