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

Definition df-thl 20423
 Description: Define the Hilbert lattice of closed subspaces of a given pre-Hilbert space. (Contributed by Mario Carneiro, 25-Oct-2015.)
Assertion
Ref Expression
df-thl toHL = ( ∈ V ↦ ((toInc‘(ClSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))

Detailed syntax breakdown of Definition df-thl
StepHypRef Expression
1 cthl 20420 . 2 class toHL
2 vh . . 3 setvar
3 cvv 3410 . . 3 class V
42cv 1538 . . . . . 6 class
5 ccss 20419 . . . . . 6 class ClSubSp
64, 5cfv 6336 . . . . 5 class (ClSubSp‘)
7 cipo 17820 . . . . 5 class toInc
86, 7cfv 6336 . . . 4 class (toInc‘(ClSubSp‘))
9 cnx 16531 . . . . . 6 class ndx
10 coc 16624 . . . . . 6 class oc
119, 10cfv 6336 . . . . 5 class (oc‘ndx)
12 cocv 20418 . . . . . 6 class ocv
134, 12cfv 6336 . . . . 5 class (ocv‘)
1411, 13cop 4529 . . . 4 class ⟨(oc‘ndx), (ocv‘)⟩
15 csts 16532 . . . 4 class sSet
168, 14, 15co 7151 . . 3 class ((toInc‘(ClSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩)
172, 3, 16cmpt 5113 . 2 class ( ∈ V ↦ ((toInc‘(ClSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
181, 17wceq 1539 1 wff toHL = ( ∈ V ↦ ((toInc‘(ClSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
 Colors of variables: wff setvar class This definition is referenced by:  thlval  20453
 Copyright terms: Public domain W3C validator