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

Definition df-hil 16982
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

Detailed syntax breakdown of Definition df-hil
StepHypRef Expression
1 chs 16979 . 2
2 vh . . . . . . 7
32cv 1653 . . . . . 6
4 cpj 16978 . . . . . 6
53, 4cfv 5501 . . . . 5
65cdm 4919 . . . 4
7 ccss 16939 . . . . 5
83, 7cfv 5501 . . . 4
96, 8wceq 1654 . . 3
10 cphl 16906 . . 3
119, 2, 10crab 2716 . 2
121, 11wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  ishil  16996
  Copyright terms: Public domain W3C validator