Metamath Proof Explorer

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 ℋ = h ∈ 𝒫 ℋ | 0 ℎ ∈ h ∧ + ℎ h × h ⊆ h ∧ ⋅ ℎ ℂ × h ⊆ h

Detailed syntax breakdown

Step Hyp Ref Expression
0 csh class S ℋ
1 vh setvar h
2 chba class ℋ
3 2 cpw class 𝒫 ℋ
4 c0v class 0 ℎ
5 1 cv setvar h
6 4 5 wcel wff 0 ℎ ∈ h
7 cva class + ℎ
8 5 5 cxp class h × h
9 7 8 cima class + ℎ h × h
10 9 5 wss wff + ℎ h × h ⊆ h
11 csm class ⋅ ℎ
12 cc class ℂ
13 12 5 cxp class ℂ × h
14 11 13 cima class ⋅ ℎ ℂ × h
15 14 5 wss wff ⋅ ℎ ℂ × h ⊆ h
16 6 10 15 w3a wff 0 ℎ ∈ h ∧ + ℎ h × h ⊆ h ∧ ⋅ ℎ ℂ × h ⊆ h
17 16 1 3 crab class h ∈ 𝒫 ℋ | 0 ℎ ∈ h ∧ + ℎ h × h ⊆ h ∧ ⋅ ℎ ℂ × h ⊆ h
18 0 17 wceq wff S ℋ = h ∈ 𝒫 ℋ | 0 ℎ ∈ h ∧ + ℎ h × h ⊆ h ∧ ⋅ ℎ ℂ × h ⊆ h