Definition df-sh 8997

Description: Define the set of subspaces of a Hilbert space. See sh 8999 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 8736	. 2 class SH
2		vh	. . . . . . 7 set h
3	2	cv 952	. . . . . 6 class h
4		chil 8727	. . . . . 6 class H~
5	3, 4	wss 2037	. . . . 5 wff h (_ H~
6		c0v 8730	. . . . . 6 class 0h
7	6, 3	wcel 955	. . . . 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 952	. . . . . . . . 9 class x
11		vy	. . . . . . . . . 10 set y
12	11	cv 952	. . . . . . . . 9 class y
13		cva 8728	. . . . . . . . 9 class +h
14	10, 12, 13	co 3948	. . . . . . . 8 class (x +h y)
15	14, 3	wcel 955	. . . . . . 7 wff (x +h y) e. h
16	15, 11, 3	wral 1637	. . . . . 6 wff A.y e. h (x +h y) e. h
17	16, 9, 3	wral 1637	. . . . 5 wff A.x e. h A.y e. h (x +h y) e. h
18		csm 8729	. . . . . . . . 9 class .h
19	10, 12, 18	co 3948	. . . . . . . 8 class (x .h y)
20	19, 3	wcel 955	. . . . . . 7 wff (x .h y) e. h
21	20, 11, 3	wral 1637	. . . . . 6 wff A.y e. h (x .h y) e. h
22		cc 5204	. . . . . 6 class CC
23	21, 9, 22	wral 1637	. . . . 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 1456	. 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 953	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 8998  sh 8999

Copyright terms: Public domain