Metamath Proof Explorer


Definition df-thl

Description: Define the Hilbert lattice of closed subspaces of a given pre-Hilbert space. (Contributed by Mario Carneiro, 25-Oct-2015)

Ref Expression
Assertion df-thl
|- toHL = ( h e. _V |-> ( ( toInc ` ( ClSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cthl
 |-  toHL
1 vh
 |-  h
2 cvv
 |-  _V
3 cipo
 |-  toInc
4 ccss
 |-  ClSubSp
5 1 cv
 |-  h
6 5 4 cfv
 |-  ( ClSubSp ` h )
7 6 3 cfv
 |-  ( toInc ` ( ClSubSp ` h ) )
8 csts
 |-  sSet
9 coc
 |-  oc
10 cnx
 |-  ndx
11 10 9 cfv
 |-  ( oc ` ndx )
12 cocv
 |-  ocv
13 5 12 cfv
 |-  ( ocv ` h )
14 11 13 cop
 |-  <. ( oc ` ndx ) , ( ocv ` h ) >.
15 7 14 8 co
 |-  ( ( toInc ` ( ClSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. )
16 1 2 15 cmpt
 |-  ( h e. _V |-> ( ( toInc ` ( ClSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. ) )
17 0 16 wceq
 |-  toHL = ( h e. _V |-> ( ( toInc ` ( ClSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. ) )