Definition df-sh 9071

Description: Define the set of subspaces of a Hilbert space. See sh 9073 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95.

Assertion

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

Distinct variable group:   x,y,h

Detailed syntax breakdown of Definition df-sh

Step	Hyp	Ref	Expression
1		csh 8792	. 2 class SH
2		vh	. . . . . . 7 set h
3	2	cv 957	. . . . . 6 class h
4		chil 8783	. . . . . 6 class H~
5	3, 4	wss 2050	. . . . 5 wff h (_ H~
6		c0v 8786	. . . . . 6 class 0h
7	6, 3	wcel 960	. . . . 5 wff 0h e. h
8	5, 7	wa 223	. . . 4 wff (h (_ H~ /\ 0h e. h)
9		vx	. . . . . . . . . 10 set x
10	9	cv 957	. . . . . . . . 9 class x
11		vy	. . . . . . . . . 10 set y
12	11	cv 957	. . . . . . . . 9 class y
13		cva 8784	. . . . . . . . 9 class +h
14	10, 12, 13	co 3969	. . . . . . . 8 class (x +h y)
15	14, 3	wcel 960	. . . . . . 7 wff (x +h y) e. h
16	15, 11, 3	wral 1648	. . . . . 6 wff A.y e. h (x +h y) e. h
17	16, 9, 3	wral 1648	. . . . 5 wff A.x e. h A.y e. h (x +h y) e. h
18		csm 8785	. . . . . . . . 9 class .h
19	10, 12, 18	co 3969	. . . . . . . 8 class (x .h y)
20	19, 3	wcel 960	. . . . . . 7 wff (x .h y) e. h
21	20, 11, 3	wral 1648	. . . . . 6 wff A.y e. h (x .h y) e. h
22		cc 5244	. . . . . 6 class CC
23	21, 9, 22	wral 1648	. . . . 5 wff A.x e. CC A.y e. h (x .h y) e. h
24	17, 23	wa 223	. . . 4 wff (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)
25	8, 24	wa 223	. . 3 wff ((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))
26	25, 2	cab 1466	. 2 class {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))}
27	1, 26	wceq 958	1 wff 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))}

This definition is referenced by:  shex 9072  sh 9073

Copyright terms: Public domain