Definition df-sh

Description: Define the set of subspaces of a Hilbert space. See issh 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.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csh	⊢ Sℋ
1		vh	⊢ ℎ
2		chba	⊢ ℋ
3	2	cpw	⊢ 𝒫 ℋ
4		c0v	⊢ 0ℎ
5	1	cv	⊢ ℎ
6	4 5	wcel	⊢ 0ℎ ∈ ℎ
7		cva	⊢ +ℎ
8	5 5	cxp	⊢ ( ℎ × ℎ )
9	7 8	cima	⊢ ( +ℎ “ ( ℎ × ℎ ) )
10	9 5	wss	⊢ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ
11		csm	⊢ ·ℎ
12		cc	⊢ ℂ
13	12 5	cxp	⊢ ( ℂ × ℎ )
14	11 13	cima	⊢ ( ·ℎ “ ( ℂ × ℎ ) )
15	14 5	wss	⊢ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ
16	6 10 15	w3a	⊢ ( 0ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ )
17	16 1 3	crab	⊢ { ℎ ∈ 𝒫 ℋ ∣ ( 0ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) }
18	0 17	wceq	⊢ Sℋ = { ℎ ∈ 𝒫 ℋ ∣ ( 0ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) }