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 ) >. ) )