MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-hil Structured version   Visualization version   GIF version

Definition df-hil 20029
Description: Define class of all Hilbert spaces. Based on Proposition 4.5, p. 176, Gudrun Kalmbach, Quantum Measures and Spaces, Kluwer, Dordrecht, 1998. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 16-Oct-2015.)
Assertion
Ref Expression
df-hil Hil = { ∈ PreHil ∣ dom (proj‘) = (CSubSp‘)}

Detailed syntax breakdown of Definition df-hil
StepHypRef Expression
1 chs 20026 . 2 class Hil
2 vh . . . . . . 7 setvar
32cv 1480 . . . . . 6 class
4 cpj 20025 . . . . . 6 class proj
53, 4cfv 5876 . . . . 5 class (proj‘)
65cdm 5104 . . . 4 class dom (proj‘)
7 ccss 19986 . . . . 5 class CSubSp
83, 7cfv 5876 . . . 4 class (CSubSp‘)
96, 8wceq 1481 . . 3 wff dom (proj‘) = (CSubSp‘)
10 cphl 19950 . . 3 class PreHil
119, 2, 10crab 2913 . 2 class { ∈ PreHil ∣ dom (proj‘) = (CSubSp‘)}
121, 11wceq 1481 1 wff Hil = { ∈ PreHil ∣ dom (proj‘) = (CSubSp‘)}
Colors of variables: wff setvar class
This definition is referenced by:  ishil  20043
  Copyright terms: Public domain W3C validator