Theorem shss 9034

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 9033	. . 3 |- (H e. SH <-> ((H (_ H~ /\ 0h e. H) /\ (A.x e. H A.y e. H (x +h y) e. H /\ A.x e. CC A.y e. H (x .h y) e. H)))
2	1	pm3.26bi 322	. 2 |- (H e. SH -> (H (_ H~ /\ 0h e. H))
3	2	pm3.26d 321	1 |- (H e. SH -> H (_ H~)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 958  A.wral 1644   (_ wss 2045  (class class class)co 3961  CCcc 5220  H~chil 8743   +h cva 8744   .h csm 8745  0hc0v 8746  SHcsh 8752

This theorem is referenced by:  shelt 9035  shssi 9036  shsubclt 9044  shsubcltOLD 9045  chss 9054  shsspwh 9073  hhsssh 9094  shocelt 9110  shocsh 9112  ocss 9113  shocss 9114  shocorth 9120  shococss 9122  shorth 9123  shocclt 9138  shselt 9233  shintcl 9248  spanid 9272  shjvalt 9276  shjclt 9283

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2701  ax-hilex 8824

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1648  df-v 1810  df-in 2049  df-ss 2051  df-sh 9031

Copyright terms: Public domain