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	⊢ Sℋ = {h∣((h ⊆ ℋ ∧ 0v ∈ h) ∧ (∀x ∈ h ∀y ∈ h (x +v y) ∈ h ∧ ∀x ∈ ℂ ∀y ∈ h (x ·s y) ∈ h))}

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

Detailed syntax breakdown of Definition df-sh

Step	Hyp	Ref	Expression
1		csh 4967	. 2 class Sℋ
2		vh	. . . . . . 7 set h
3	2	cv 1089	. . . . . 6 class h
4		chil 4958	. . . . . 6 class ℋ
5	3, 4	wss 1487	. . . . 5 wff h ⊆ ℋ
6		c0v 4961	. . . . . 6 class 0v
7	6, 3	wcel 1092	. . . . 5 wff 0v ∈ h
8	5, 7	wa 196	. . . 4 wff (h ⊆ ℋ ∧ 0v ∈ 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) ∈ h
16	15, 11, 3	wral 1201	. . . . . 6 wff ∀y ∈ h (x +v y) ∈ h
17	16, 9, 3	wral 1201	. . . . 5 wff ∀x ∈ h ∀y ∈ h (x +v y) ∈ 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) ∈ h
21	20, 11, 3	wral 1201	. . . . . 6 wff ∀y ∈ h (x ·s y) ∈ h
22		cc 4026	. . . . . 6 class ℂ
23	21, 9, 22	wral 1201	. . . . 5 wff ∀x ∈ ℂ ∀y ∈ h (x ·s y) ∈ h
24	17, 23	wa 196	. . . 4 wff (∀x ∈ h ∀y ∈ h (x +v y) ∈ h ∧ ∀x ∈ ℂ ∀y ∈ h (x ·s y) ∈ h)
25	8, 24	wa 196	. . 3 wff ((h ⊆ ℋ ∧ 0v ∈ h) ∧ (∀x ∈ h ∀y ∈ h (x +v y) ∈ h ∧ ∀x ∈ ℂ ∀y ∈ h (x ·s y) ∈ h))
26	25, 2	cab 1090	. 2 class {h∣((h ⊆ ℋ ∧ 0v ∈ h) ∧ (∀x ∈ h ∀y ∈ h (x +v y) ∈ h ∧ ∀x ∈ ℂ ∀y ∈ h (x ·s y) ∈ h))}
27	1, 26	wceq 1091	1 wff Sℋ = {h∣((h ⊆ ℋ ∧ 0v ∈ h) ∧ (∀x ∈ h ∀y ∈ h (x +v y) ∈ h ∧ ∀x ∈ ℂ ∀y ∈ h (x ·s y) ∈ h))}

This definition is referenced by:  shex 5115  sh 5116

metamath.org