Theorem sh 9017

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 1813	. 2 |- (H e. SH -> H e. V)
2		ax-hilex 8808	. . . 4 |- H~ e. V
3	2	ssex 2714	. . 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 2078	. . . . 5 |- (h = H -> (h (_ H~ <-> H (_ H~))
6		eleq2 1532	. . . . 5 |- (h = H -> (0h e. h <-> 0h e. H))
7	5, 6	anbi12d 627	. . . 4 |- (h = H -> ((h (_ H~ /\ 0h e. h) <-> (H (_ H~ /\ 0h e. H)))
8		eleq2 1532	. . . . . . 7 |- (h = H -> ((x +h y) e. h <-> (x +h y) e. H))
9	8	raleqd 1788	. . . . . 6 |- (h = H -> (A.y e. h (x +h y) e. h <-> A.y e. H (x +h y) e. H))
10	9	raleqd 1788	. . . . 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 1532	. . . . . . 7 |- (h = H -> ((x .h y) e. h <-> (x .h y) e. H))
12	11	raleqd 1788	. . . . . 6 |- (h = H -> (A.y e. h (x .h y) e. h <-> A.y e. H (x .h y) e. H))
13	12	ralbidv 1660	. . . . 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 627	. . . 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 627	. . 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 9015	. . 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 1896	. 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 678	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 954   e. wcel 956  A.wral 1642  Vcvv 1807   (_ wss 2043  (class class class)co 3954  CCcc 5212  H~chil 8727   +h cva 8728   .h csm 8729  0hc0v 8730  SHcsh 8736

This theorem is referenced by:  shss 9018  sh0 9023  shaddclt 9024  shaddcltOLD 9025  shmulclt 9026  shmulcltOLD 9027  sh2 9030  helch 9055  hsn0elch 9059  hhshsslem2 9077  ocsh 9095  shscl 9219  shintcl 9231

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-hilex 8808

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ral 1646  df-v 1808  df-in 2047  df-ss 2049  df-sh 9015

Copyright terms: Public domain