Theorem cheli 29003

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

Syntax hints:   → wi 4   ∈ wcel 2110   ℋchba 28690   C_ℋ cch 28700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-hilex 28770

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-xp 5556  df-cnv 5558  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fv 6358  df-ov 7153  df-sh 28978  df-ch 28992

This theorem is referenced by:  pjhthlem1  29162  pjhthlem2  29163  h1de2ci  29327  spanunsni  29350  spansncvi  29423  3oalem1  29433  pjcompi  29443  pjocini  29469  pjjsi  29471  pjrni  29473  pjdsi  29483  pjds3i  29484  mayete3i  29499  riesz3i  29833  pjnmopi  29919  pjnormssi  29939  pjimai  29947  pjclem4a  29969  pjclem4  29970  pj3lem1  29977  pj3si  29978  strlem1  30021  strlem3  30024  strlem5  30026  hstrlem3  30032  hstrlem5  30034  sumdmdii  30186  sumdmdlem  30189  sumdmdlem2  30190