Theorem sh 9078

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 1817	. 2 |- (H e. SH -> H e. V)
2		ax-hilex 8869	. . . 4 |- H~ e. V
3	2	ssex 2719	. . 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 2082	. . . . 5 |- (h = H -> (h (_ H~ <-> H (_ H~))
6		eleq2 1535	. . . . 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 1535	. . . . . . 7 |- (h = H -> ((x +h y) e. h <-> (x +h y) e. H))
9	8	raleqd 1791	. . . . . 6 |- (h = H -> (A.y e. h (x +h y) e. h <-> A.y e. H (x +h y) e. H))
10	9	raleqd 1791	. . . . 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 1535	. . . . . . 7 |- (h = H -> ((x .h y) e. h <-> (x .h y) e. H))
12	11	raleqd 1791	. . . . . 6 |- (h = H -> (A.y e. h (x .h y) e. h <-> A.y e. H (x .h y) e. H))
13	12	ralbidv 1663	. . . . 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 9076	. . 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 1900	. 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 1645  Vcvv 1811   (_ wss 2047  (class class class)co 3963  CCcc 5232  H~chil 8788   +h cva 8789   .h csm 8790  0hc0v 8791  SHcsh 8797

This theorem is referenced by:  shss 9079  sh0 9084  shaddclt 9085  shaddcltOLD 9086  shmulclt 9087  shmulcltOLD 9088  sh2 9091  helch 9116  hsn0elch 9120  hhshsslem2 9138  ocsh 9156  shscl 9281  shintcl 9293

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 2703  ax-hilex 8869

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 1649  df-v 1812  df-in 2051  df-ss 2053  df-sh 9076

Copyright terms: Public domain