Theorem cheli 29594

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

Syntax hints:   → wi 4   ∈ wcel 2106   ℋchba 29281   C_ℋ cch 29291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-hilex 29361

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fv 6441  df-ov 7278  df-sh 29569  df-ch 29583

This theorem is referenced by:  pjhthlem1  29753  pjhthlem2  29754  h1de2ci  29918  spanunsni  29941  spansncvi  30014  3oalem1  30024  pjcompi  30034  pjocini  30060  pjjsi  30062  pjrni  30064  pjdsi  30074  pjds3i  30075  mayete3i  30090  riesz3i  30424  pjnmopi  30510  pjnormssi  30530  pjimai  30538  pjclem4a  30560  pjclem4  30561  pj3lem1  30568  pj3si  30569  strlem1  30612  strlem3  30615  strlem5  30617  hstrlem3  30623  hstrlem5  30625  sumdmdii  30777  sumdmdlem  30780  sumdmdlem2  30781