HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-sh Structured version   Visualization version   GIF version

Definition df-sh 28192
Description: Define the set of subspaces of a Hilbert space. See issh 28193 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
StepHypRef Expression
1 csh 27913 . 2 class S
2 c0v 27909 . . . . 5 class 0
3 vh . . . . . 6 setvar
43cv 1522 . . . . 5 class
52, 4wcel 2030 . . . 4 wff 0
6 cva 27905 . . . . . 6 class +
74, 4cxp 5141 . . . . . 6 class ( × )
86, 7cima 5146 . . . . 5 class ( + “ ( × ))
98, 4wss 3607 . . . 4 wff ( + “ ( × )) ⊆
10 csm 27906 . . . . . 6 class ·
11 cc 9972 . . . . . . 7 class
1211, 4cxp 5141 . . . . . 6 class (ℂ × )
1310, 12cima 5146 . . . . 5 class ( · “ (ℂ × ))
1413, 4wss 3607 . . . 4 wff ( · “ (ℂ × )) ⊆
155, 9, 14w3a 1054 . . 3 wff (0 ∧ ( + “ ( × )) ⊆ ∧ ( · “ (ℂ × )) ⊆ )
16 chil 27904 . . . 4 class
1716cpw 4191 . . 3 class 𝒫 ℋ
1815, 3, 17crab 2945 . 2 class { ∈ 𝒫 ℋ ∣ (0 ∧ ( + “ ( × )) ⊆ ∧ ( · “ (ℂ × )) ⊆ )}
191, 18wceq 1523 1 wff S = { ∈ 𝒫 ℋ ∣ (0 ∧ ( + “ ( × )) ⊆ ∧ ( · “ (ℂ × )) ⊆ )}
Colors of variables: wff setvar class
This definition is referenced by:  issh  28193
  Copyright terms: Public domain W3C validator