Theorem cheli 29580

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

Syntax hints:   → wi 4   ∈ wcel 2106   ℋchba 29267   C_ℋ cch 29277

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 5222  ax-hilex 29347

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 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5075  df-opab 5137  df-xp 5591  df-cnv 5593  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6385  df-fv 6435  df-ov 7271  df-sh 29555  df-ch 29569

This theorem is referenced by:  pjhthlem1  29739  pjhthlem2  29740  h1de2ci  29904  spanunsni  29927  spansncvi  30000  3oalem1  30010  pjcompi  30020  pjocini  30046  pjjsi  30048  pjrni  30050  pjdsi  30060  pjds3i  30061  mayete3i  30076  riesz3i  30410  pjnmopi  30496  pjnormssi  30516  pjimai  30524  pjclem4a  30546  pjclem4  30547  pj3lem1  30554  pj3si  30555  strlem1  30598  strlem3  30601  strlem5  30603  hstrlem3  30609  hstrlem5  30611  sumdmdii  30763  sumdmdlem  30766  sumdmdlem2  30767