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

Definition df-hil 16604
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  =  { h  e.  PreHil  |  dom  ( proj `  h )  =  ( CSubSp `  h
) }

Detailed syntax breakdown of Definition df-hil
StepHypRef Expression
1 chs 16601 . 2  class  Hil
2 vh . . . . . . 7  set  h
32cv 1622 . . . . . 6  class  h
4 cpj 16600 . . . . . 6  class  proj
53, 4cfv 5255 . . . . 5  class  ( proj `  h )
65cdm 4689 . . . 4  class  dom  ( proj `  h )
7 ccss 16561 . . . . 5  class  CSubSp
83, 7cfv 5255 . . . 4  class  ( CSubSp `  h )
96, 8wceq 1623 . . 3  wff  dom  ( proj `  h )  =  ( CSubSp `  h )
10 cphl 16528 . . 3  class  PreHil
119, 2, 10crab 2547 . 2  class  { h  e.  PreHil  |  dom  ( proj `  h )  =  ( CSubSp `  h ) }
121, 11wceq 1623 1  wff  Hil  =  { h  e.  PreHil  |  dom  ( proj `  h )  =  ( CSubSp `  h
) }
Colors of variables: wff set class
This definition is referenced by:  ishil  16618
  Copyright terms: Public domain W3C validator