Theorem shss 5117

Description: A subspace is a subset of Hilbert space.

Assertion

Ref	Expression
shss	|- (H e. SH -> H (_ H~)

Proof of Theorem shss

Step	Hyp	Ref	Expression
1		sh 5116	. . 3 |- (H e. SH <-> ((H (_ H~ /\ 0v e. H) /\ (A.x e. H A.y e. H (x +v y) e. H /\ A.x e. CC A.y e. H (x .s y) e. H)))
2	1	pm3.26bd 259	. 2 |- (H e. SH -> (H (_ H~ /\ 0v e. H))
3	2	pm3.26d 258	1 |- (H e. SH -> H (_ H~)

Syntax hints:   -> wi 2   /\ wa 196   e. wcel 1092  A.wral 1201   (_ wss 1487  (class class class)co 3001  CCcc 4026  H~chil 4958   +v cva 4959   .s csm 4960  0vc0v 4961  SHcsh 4967

This theorem is referenced by:  shelt 5118  shssi 5119  shsubclt 5125  chss 5134  shsspwh 5153  shocelt 5163  shocsh 5165  ocss 5166  shocss 5167  shocorth 5173  shococss 5175  shorth 5176  shocclt 5190  shselt 5280  shintcl 5294  spanid 5318  shjvalt 5322  shjclt 5329  spansnsst 5476

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

metamath.org