Definition df-sh 5114

Description: Define the set of subspaces of a Hilbert space. See sh 5116 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~ /\ 0v e. h) /\ (A.x e. h A.y e. h (x +v y) e. h /\ A.x e. CC A.y e. h (x .s y) e. h))}

Distinct variable group(s):   x,y,h

Detailed syntax breakdown of Definition df-sh

Step	Hyp	Ref	Expression
1		csh 4967	. 2 class SH
2		vh	. . . . . . 7 set h
3	2	cv 1089	. . . . . 6 class h
4		chil 4958	. . . . . 6 class H~
5	3, 4	wss 1487	. . . . 5 wff h (_ H~
6		c0v 4961	. . . . . 6 class 0v
7	6, 3	wcel 1092	. . . . 5 wff 0v e. h
8	5, 7	wa 196	. . . 4 wff (h (_ H~ /\ 0v e. h)
9		vx	. . . . . . . . . 10 set x
10	9	cv 1089	. . . . . . . . 9 class x
11		vy	. . . . . . . . . 10 set y
12	11	cv 1089	. . . . . . . . 9 class y
13		cva 4959	. . . . . . . . 9 class +v
14	10, 12, 13	co 3001	. . . . . . . 8 class (x +v y)
15	14, 3	wcel 1092	. . . . . . 7 wff (x +v y) e. h
16	15, 11, 3	wral 1201	. . . . . 6 wff A.y e. h (x +v y) e. h
17	16, 9, 3	wral 1201	. . . . 5 wff A.x e. h A.y e. h (x +v y) e. h
18		csm 4960	. . . . . . . . 9 class .s
19	10, 12, 18	co 3001	. . . . . . . 8 class (x .s y)
20	19, 3	wcel 1092	. . . . . . 7 wff (x .s y) e. h
21	20, 11, 3	wral 1201	. . . . . 6 wff A.y e. h (x .s y) e. h
22		cc 4026	. . . . . 6 class CC
23	21, 9, 22	wral 1201	. . . . 5 wff A.x e. CC A.y e. h (x .s y) e. h
24	17, 23	wa 196	. . . 4 wff (A.x e. h A.y e. h (x +v y) e. h /\ A.x e. CC A.y e. h (x .s y) e. h)
25	8, 24	wa 196	. . 3 wff ((h (_ H~ /\ 0v e. h) /\ (A.x e. h A.y e. h (x +v y) e. h /\ A.x e. CC A.y e. h (x .s y) e. h))
26	25, 2	cab 1090	. 2 class {h | ((h (_ H~ /\ 0v e. h) /\ (A.x e. h A.y e. h (x +v y) e. h /\ A.x e. CC A.y e. h (x .s y) e. h))}
27	1, 26	wceq 1091	1 wff SH = {h | ((h (_ H~ /\ 0v e. h) /\ (A.x e. h A.y e. h (x +v y) e. h /\ A.x e. CC A.y e. h (x .s y) e. h))}

This definition is referenced by:  shex 5115  sh 5116

metamath.org