Definition df-sh 31818

Description: Define the set of subspaces of a Hilbert space. See issh 31819 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. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
df-sh	⊢ Sℋ = {ℎ ∈ 𝒫 ℋ ∣ (0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ “ (ℂ × ℎ)) ⊆ ℎ)}

Detailed syntax breakdown of Definition df-sh

Step	Hyp	Ref	Expression
1		csh 31539	. 2 class Sℋ
2		c0v 31535	. . . . 5 class 0ℎ
3		vh	. . . . . 6 setvar ℎ
4	3	cv 1568	. . . . 5 class ℎ
5	2, 4	wcel 2144	. . . 4 wff 0ℎ ∈ ℎ
6		cva 31531	. . . . . 6 class +ℎ
7	4, 4	cxp 5649	. . . . . 6 class (ℎ × ℎ)
8	6, 7	cima 5654	. . . . 5 class ( +ℎ “ (ℎ × ℎ))
9	8, 4	wss 3896	. . . 4 wff ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ
10		csm 31532	. . . . . 6 class ·ℎ
11		cc 11205	. . . . . . 7 class ℂ
12	11, 4	cxp 5649	. . . . . 6 class (ℂ × ℎ)
13	10, 12	cima 5654	. . . . 5 class ( ·ℎ “ (ℂ × ℎ))
14	13, 4	wss 3896	. . . 4 wff ( ·ℎ “ (ℂ × ℎ)) ⊆ ℎ
15	5, 9, 14	w3a 1103	. . 3 wff (0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ “ (ℂ × ℎ)) ⊆ ℎ)
16		chba 31530	. . . 4 class ℋ
17	16	cpw 4556	. . 3 class 𝒫 ℋ
18	15, 3, 17	crab 3412	. 2 class {ℎ ∈ 𝒫 ℋ ∣ (0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ “ (ℂ × ℎ)) ⊆ ℎ)}
19	1, 18	wceq 1569	1 wff Sℋ = {ℎ ∈ 𝒫 ℋ ∣ (0ℎ ∈ ℎ ∧ ( +ℎ “ (ℎ × ℎ)) ⊆ ℎ ∧ ( ·ℎ “ (ℂ × ℎ)) ⊆ ℎ)}

This definition is used by:  issh  31819