Theorem sh 10711

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 C_ ~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 2299	. 2 |- (H e. SH -> H e. _V)
2		ax-hilex 10501	. . . 4 |- ~H e. _V
3	2	ssex 3455	. . 3 |- (H C_ ~H -> H e. _V)
4	3	ad2antrr 440	. 2 |- (((H C_ ~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 2637	. . . . 5 |- (h = H -> (h C_ ~H <-> H C_ ~H))
6		eleq2 1958	. . . . 5 |- (h = H -> (0h e. h <-> 0h e. H))
7	5, 6	anbi12d 690	. . . 4 |- (h = H -> ((h C_ ~H /\ 0h e. h) <-> (H C_ ~H /\ 0h e. H)))
8		eleq2 1958	. . . . . . 7 |- (h = H -> ((x +h y) e. h <-> (x +h y) e. H))
9	8	raleqbi1dv 2271	. . . . . 6 |- (h = H -> (A.y e. h (x +h y) e. h <-> A.y e. H (x +h y) e. H))
10	9	raleqbi1dv 2271	. . . . 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 1958	. . . . . . 7 |- (h = H -> ((x .h y) e. h <-> (x .h y) e. H))
12	11	raleqbi1dv 2271	. . . . . 6 |- (h = H -> (A.y e. h (x .h y) e. h <-> A.y e. H (x .h y) e. H))
13	12	ralbidv 2123	. . . . 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 690	. . . 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 690	. . 3 |- (h = H -> (((h C_ ~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 C_ ~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 10709	. . 3 |- SH = {h | ((h C_ ~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 2406	. 2 |- (H e. _V -> (H e. SH <-> ((H C_ ~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 743	1 |- (H e. SH <-> ((H C_ ~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 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593  (class class class)co 4884  CCcc 6384  ~Hchil 10420   +h cva 10421   .h csm 10422  0hc0v 10423  SHcsh 10429

This theorem is referenced by:  shss 10712  sh0 10717  shaddcl 10718  shaddclOLD 10719  shmulcl 10720  shmulclOLD 10721  sh2 10724  helch 10749  hsn0elch 10753  hhshsslem2 10771  ocsh 10789  shscli 10914  shintcli 10926

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-hilex 10501

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-v 2294  df-in 2603  df-ss 2605  df-sh 10709

Copyright terms: Public domain