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

Definition df-hil 16962
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 16959 . 2  class  Hil
2 vh . . . . . . 7  set  h
32cv 1652 . . . . . 6  class  h
4 cpj 16958 . . . . . 6  class  proj
53, 4cfv 5483 . . . . 5  class  ( proj `  h )
65cdm 4907 . . . 4  class  dom  ( proj `  h )
7 ccss 16919 . . . . 5  class  CSubSp
83, 7cfv 5483 . . . 4  class  ( CSubSp `  h )
96, 8wceq 1653 . . 3  wff  dom  ( proj `  h )  =  ( CSubSp `  h )
10 cphl 16886 . . 3  class  PreHil
119, 2, 10crab 2715 . 2  class  { h  e.  PreHil  |  dom  ( proj `  h )  =  ( CSubSp `  h ) }
121, 11wceq 1653 1  wff  Hil  =  { h  e.  PreHil  |  dom  ( proj `  h )  =  ( CSubSp `  h
) }
Colors of variables: wff set class
This definition is referenced by:  ishil  16976
  Copyright terms: Public domain W3C validator