Theorem cheli 31714

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ℋchba 31401   C_ℋ cch 31411

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-hilex 31481

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fv 6541  df-ov 7417  df-sh 31689  df-ch 31703

This theorem is used by:  pjhthlem1  31873  pjhthlem2  31874  h1de2ci  32038  spanunsni  32061  spansncvi  32134  3oalem1  32144  pjcompi  32154  pjocini  32180  pjjsi  32182  pjrni  32184  pjdsi  32194  pjds3i  32195  mayete3i  32210  riesz3i  32544  pjnmopi  32630  pjnormssi  32650  pjimai  32658  pjclem4a  32680  pjclem4  32681  pj3lem1  32688  pj3si  32689  strlem1  32732  strlem3  32735  strlem5  32737  hstrlem3  32743  hstrlem5  32745  sumdmdii  32897  sumdmdlem  32900  sumdmdlem2  32901