Definition df-sh 9031

Description: Define the set of subspaces of a Hilbert space. See sh 9033 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 ⊆ ℋ ⋀ 0h ∈ h) ⋀ (∀x ∈ h ∀y ∈ h (x +h y) ∈ h ⋀ ∀x ∈ ℂ ∀y ∈ h (x ·h y) ∈ h))}

Distinct variable group:   x,y,h

Detailed syntax breakdown of Definition df-sh

Step	Hyp	Ref	Expression
1		csh 8752	. 2 class Sℋ
2		vh	. . . . . . 7 set h
3	2	cv 954	. . . . . 6 class h
4		chil 8743	. . . . . 6 class ℋ
5	3, 4	wss 2044	. . . . 5 wff h ⊆ ℋ
6		c0v 8746	. . . . . 6 class 0h
7	6, 3	wcel 957	. . . . 5 wff 0h ∈ h
8	5, 7	wa 223	. . . 4 wff (h ⊆ ℋ ⋀ 0h ∈ h)
9		vx	. . . . . . . . . 10 set x
10	9	cv 954	. . . . . . . . 9 class x
11		vy	. . . . . . . . . 10 set y
12	11	cv 954	. . . . . . . . 9 class y
13		cva 8744	. . . . . . . . 9 class +h
14	10, 12, 13	co 3958	. . . . . . . 8 class (x +h y)
15	14, 3	wcel 957	. . . . . . 7 wff (x +h y) ∈ h
16	15, 11, 3	wral 1643	. . . . . 6 wff ∀y ∈ h (x +h y) ∈ h
17	16, 9, 3	wral 1643	. . . . 5 wff ∀x ∈ h ∀y ∈ h (x +h y) ∈ h
18		csm 8745	. . . . . . . . 9 class ·h
19	10, 12, 18	co 3958	. . . . . . . 8 class (x ·h y)
20	19, 3	wcel 957	. . . . . . 7 wff (x ·h y) ∈ h
21	20, 11, 3	wral 1643	. . . . . 6 wff ∀y ∈ h (x ·h y) ∈ h
22		cc 5215	. . . . . 6 class ℂ
23	21, 9, 22	wral 1643	. . . . 5 wff ∀x ∈ ℂ ∀y ∈ h (x ·h y) ∈ h
24	17, 23	wa 223	. . . 4 wff (∀x ∈ h ∀y ∈ h (x +h y) ∈ h ⋀ ∀x ∈ ℂ ∀y ∈ h (x ·h y) ∈ h)
25	8, 24	wa 223	. . 3 wff ((h ⊆ ℋ ⋀ 0h ∈ h) ⋀ (∀x ∈ h ∀y ∈ h (x +h y) ∈ h ⋀ ∀x ∈ ℂ ∀y ∈ h (x ·h y) ∈ h))
26	25, 2	cab 1462	. 2 class {h∣((h ⊆ ℋ ⋀ 0h ∈ h) ⋀ (∀x ∈ h ∀y ∈ h (x +h y) ∈ h ⋀ ∀x ∈ ℂ ∀y ∈ h (x ·h y) ∈ h))}
27	1, 26	wceq 955	1 wff Sℋ = {h∣((h ⊆ ℋ ⋀ 0h ∈ h) ⋀ (∀x ∈ h ∀y ∈ h (x +h y) ∈ h ⋀ ∀x ∈ ℂ ∀y ∈ h (x ·h y) ∈ h))}

This definition is referenced by:  shex 9032  sh 9033

Copyright terms: Public domain