Theorem sh 8999

Description: Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95.

Assertion

Ref	Expression
sh	|- (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)))

Distinct variable group:   x,y,H

Proof of Theorem sh

Step	Hyp	Ref	Expression
1		elisset 1808	. 2 |- (H e. SH -> H e. V)
2		ax-hilex 8790	. . . 4 |- H~ e. V
3	2	ssex 2709	. . 3 |- (H (_ H~ -> H e. V)
4	3	ad2antrr 404	. 2 |- (((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)) -> H e. V)
5		sseq1 2072	. . . . 5 |- (h = H -> (h (_ H~ <-> H (_ H~))
6		eleq2 1527	. . . . 5 |- (h = H -> (0h e. h <-> 0h e. H))
7	5, 6	anbi12d 626	. . . 4 |- (h = H -> ((h (_ H~ /\ 0h e. h) <-> (H (_ H~ /\ 0h e. H)))
8		eleq2 1527	. . . . . . 7 |- (h = H -> ((x +h y) e. h <-> (x +h y) e. H))
9	8	raleqd 1783	. . . . . 6 |- (h = H -> (A.y e. h (x +h y) e. h <-> A.y e. H (x +h y) e. H))
10	9	raleqd 1783	. . . . 5 |- (h = H -> (A.x e. h A.y e. h (x +h y) e. h <-> A.x e. H A.y e. H (x +h y) e. H))
11		eleq2 1527	. . . . . . 7 |- (h = H -> ((x .h y) e. h <-> (x .h y) e. H))
12	11	raleqd 1783	. . . . . 6 |- (h = H -> (A.y e. h (x .h y) e. h <-> A.y e. H (x .h y) e. H))
13	12	ralbidv 1655	. . . . 5 |- (h = H -> (A.x e. CC A.y e. h (x .h y) e. h <-> A.x e. CC A.y e. H (x .h y) e. H))
14	10, 13	anbi12d 626	. . . 4 |- (h = 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) <-> (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)))
15	7, 14	anbi12d 626	. . 3 |- (h = H -> (((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)) <-> ((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))))
16		df-sh 8997	. . 3 |- SH = {h | ((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))}
17	15, 16	elab2g 1891	. 2 |- (H e. V -> (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))))
18	1, 4, 17	pm5.21nii 677	1 |- (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)))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  A.wral 1637  Vcvv 1802   (_ wss 2037  (class class class)co 3948  CCcc 5204  H~chil 8727   +h cva 8728   .h csm 8729  0hc0v 8730  SHcsh 8736

This theorem is referenced by:  shss 9000  sh0 9005  shaddclt 9006  shaddcltOLD 9007  shmulclt 9008  shmulcltOLD 9009  sh2 9012  helch 9037  hsn0elch 9041  hhshsslem2 9058  ocsh 9072  shscl 9196  shintcl 9208

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-hilex 8790

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ral 1641  df-v 1803  df-in 2041  df-ss 2043  df-sh 8997

Copyright terms: Public domain