Theorem cheli 28607

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

Syntax hints:   → wi 4   ∈ wcel 2157   ℋchba 28294   C_ℋ cch 28304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-hilex 28374

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-rex 3094  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4628  df-br 4843  df-opab 4905  df-xp 5317  df-cnv 5319  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6063  df-fv 6108  df-ov 6880  df-sh 28582  df-ch 28596

This theorem is referenced by:  pjhthlem1  28768  pjhthlem2  28769  h1de2ci  28933  spanunsni  28956  spansncvi  29029  3oalem1  29039  pjcompi  29049  pjocini  29075  pjjsi  29077  pjrni  29079  pjdsi  29089  pjds3i  29090  mayete3i  29105  riesz3i  29439  pjnmopi  29525  pjnormssi  29545  pjimai  29553  pjclem4a  29575  pjclem4  29576  pj3lem1  29583  pj3si  29584  strlem1  29627  strlem3  29630  strlem5  29632  hstrlem3  29638  hstrlem5  29640  sumdmdii  29792  sumdmdlem  29795  sumdmdlem2  29796