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 20402
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‘) = (ClSubSp‘)}

Detailed syntax breakdown of Definition df-hil
StepHypRef Expression
1 chil 20399 . 2 class Hil
2 vh . . . . . . 7 setvar
32cv 1537 . . . . . 6 class
4 cpj 20398 . . . . . 6 class proj
53, 4cfv 6345 . . . . 5 class (proj‘)
65cdm 5543 . . . 4 class dom (proj‘)
7 ccss 20359 . . . . 5 class ClSubSp
83, 7cfv 6345 . . . 4 class (ClSubSp‘)
96, 8wceq 1538 . . 3 wff dom (proj‘) = (ClSubSp‘)
10 cphl 20322 . . 3 class PreHil
119, 2, 10crab 3137 . 2 class { ∈ PreHil ∣ dom (proj‘) = (ClSubSp‘)}
121, 11wceq 1538 1 wff Hil = { ∈ PreHil ∣ dom (proj‘) = (ClSubSp‘)}
Colors of variables: wff setvar class
This definition is referenced by:  ishil  20416
  Copyright terms: Public domain W3C validator