Theorem chssi 5136

Description: A closed subspace of a Hilbert space is a subset of Hilbert space.

Hypothesis

Ref	Expression
chssi.1	|- H e. CH

Assertion

Ref	Expression
chssi	|- H (_ H~

Proof of Theorem chssi

Step	Hyp	Ref	Expression
1		chssi.1	. . 3 |- H e. CH
2	1	chshi 5132	. 2 |- H e. SH
3	2	shssi 5119	1 |- H (_ H~

Syntax hints:   e. wcel 1092   (_ wss 1487  H~chil 4958  CHcch 4968

This theorem is referenced by:  chel 5137  cheli 5138  chocval 5178  chocl 5192  projlem26 5218  projlem29 5221  shlub 5347  chm1 5378  chsscon3 5383  chj1 5410  shjshs 5412  sshhococ 5451  h1det 5455  spansnpj 5481  spanunsn 5482  h1datom 5483  osumlem4 5533  osumlem8 5537  osum 5538  spansnj 5539  pjf 5588  pjocco 5643  stcltr2 5708  mdsym 5784

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-hilex 4983

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349  df-in 1491  df-ss 1492  df-sh 5114  df-ch 5127

metamath.org