Theorem cheli 29495

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

Syntax hints:   → wi 4   ∈ wcel 2108   ℋchba 29182   C_ℋ cch 29192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-hilex 29262

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fv 6426  df-ov 7258  df-sh 29470  df-ch 29484

This theorem is referenced by:  pjhthlem1  29654  pjhthlem2  29655  h1de2ci  29819  spanunsni  29842  spansncvi  29915  3oalem1  29925  pjcompi  29935  pjocini  29961  pjjsi  29963  pjrni  29965  pjdsi  29975  pjds3i  29976  mayete3i  29991  riesz3i  30325  pjnmopi  30411  pjnormssi  30431  pjimai  30439  pjclem4a  30461  pjclem4  30462  pj3lem1  30469  pj3si  30470  strlem1  30513  strlem3  30516  strlem5  30518  hstrlem3  30524  hstrlem5  30526  sumdmdii  30678  sumdmdlem  30681  sumdmdlem2  30682