Theorem sh 9033

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 1815	. 2 |- (H e. SH -> H e. V)
2		ax-hilex 8824	. . . 4 |- H~ e. V
3	2	ssex 2717	. . 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 2080	. . . . 5 |- (h = H -> (h (_ H~ <-> H (_ H~))
6		eleq2 1534	. . . . 5 |- (h = H -> (0h e. h <-> 0h e. H))
7	5, 6	anbi12d 628	. . . 4 |- (h = H -> ((h (_ H~ /\ 0h e. h) <-> (H (_ H~ /\ 0h e. H)))
8		eleq2 1534	. . . . . . 7 |- (h = H -> ((x +h y) e. h <-> (x +h y) e. H))
9	8	raleqd 1790	. . . . . 6 |- (h = H -> (A.y e. h (x +h y) e. h <-> A.y e. H (x +h y) e. H))
10	9	raleqd 1790	. . . . 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 1534	. . . . . . 7 |- (h = H -> ((x .h y) e. h <-> (x .h y) e. H))
12	11	raleqd 1790	. . . . . 6 |- (h = H -> (A.y e. h (x .h y) e. h <-> A.y e. H (x .h y) e. H))
13	12	ralbidv 1662	. . . . 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 628	. . . 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 628	. . 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 9031	. . 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 1898	. 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 679	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 956   e. wcel 958  A.wral 1644  Vcvv 1809   (_ 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:  shss 9034  sh0 9039  shaddclt 9040  shaddcltOLD 9041  shmulclt 9042  shmulcltOLD 9043  sh2 9046  helch 9071  hsn0elch 9075  hhshsslem2 9093  ocsh 9111  shscl 9236  shintcl 9248

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