Theorem chel 9097

Description: A member of a closed subspace of a Hilbert space is a vector.

Hypothesis

Ref	Expression
chssi.1	|- H e. CH

Assertion

Ref	Expression
chel	|- (A e. H -> A e. H~)

Proof of Theorem chel

Step	Hyp	Ref	Expression
1		chssi.1	. . 3 |- H e. CH
2	1	chssi 9096	. 2 |- H (_ H~
3	2	sseli 2068	1 |- (A e. H -> A e. H~)

Syntax hints:   -> wi 3   e. wcel 960  H~chil 8783  CHcch 8793

This theorem is referenced by:  hhsscms 9145  chocuni 9167  projlem8 9188  projlem10 9190  projlem12 9192  projlem13 9193  projlem15 9195  projlem26 9206  projlem28 9208  projlemHIL 9213  pjtheu2 9245  pjpj0 9250  h1de2ct 9474  spanunsn 9497  osumlem1 9573  spansncv 9592  3oalem1 9602  pjocin 9638  pjjs 9640  pjrn 9642  pjv 9645  pjds 9652  pjds3 9653  mayete3 9668  riesz3 9990  pjnmop 10070  pjnormss 10091  pjima 10099  pjclem4a 10121  pjclem4 10122  pj3lem1 10129  pj3s 10130  strlem1 10172  strlem3 10175  strlem5 10177  hstrlem3 10183  hstrlem5 10185  sumdmdi 10337  sumdmdlem 10340  sumdmdlem2 10341

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-hilex 8864

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815  df-in 2054  df-ss 2056  df-sh 9071  df-ch 9087

Copyright terms: Public domain