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

Definition df-thl 20801
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 20798 . 2 class toHL
2 vh . . 3 setvar
3 cvv 3493 . . 3 class V
42cv 1530 . . . . . 6 class
5 ccss 20797 . . . . . 6 class ClSubSp
64, 5cfv 6348 . . . . 5 class (ClSubSp‘)
7 cipo 17753 . . . . 5 class toInc
86, 7cfv 6348 . . . 4 class (toInc‘(ClSubSp‘))
9 cnx 16472 . . . . . 6 class ndx
10 coc 16565 . . . . . 6 class oc
119, 10cfv 6348 . . . . 5 class (oc‘ndx)
12 cocv 20796 . . . . . 6 class ocv
134, 12cfv 6348 . . . . 5 class (ocv‘)
1411, 13cop 4565 . . . 4 class ⟨(oc‘ndx), (ocv‘)⟩
15 csts 16473 . . . 4 class sSet
168, 14, 15co 7148 . . 3 class ((toInc‘(ClSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩)
172, 3, 16cmpt 5137 . 2 class ( ∈ V ↦ ((toInc‘(ClSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
181, 17wceq 1531 1 wff toHL = ( ∈ V ↦ ((toInc‘(ClSubSp‘)) sSet ⟨(oc‘ndx), (ocv‘)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  thlval  20831
  Copyright terms: Public domain W3C validator