Definition df-thl 20009

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

Assertion

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

Detailed syntax breakdown of Definition df-thl

Step	Hyp	Ref	Expression
1		cthl 20006	. 2 class toHL
2		vh	. . 3 setvar h
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . 6 class h
5		ccss 20005	. . . . . 6 class CSubSp
6	4, 5	cfv 5888	. . . . 5 class ( CSubSp ` h )
7		cipo 17151	. . . . 5 class toInc
8	6, 7	cfv 5888	. . . 4 class (toInc ` ( CSubSp ` h ) )
9		cnx 15854	. . . . . 6 class ndx
10		coc 15949	. . . . . 6 class oc
11	9, 10	cfv 5888	. . . . 5 class ( oc ` ndx )
12		cocv 20004	. . . . . 6 class ocv
13	4, 12	cfv 5888	. . . . 5 class ( ocv ` h )
14	11, 13	cop 4183	. . . 4 class <. ( oc ` ndx ) , ( ocv ` h ) >.
15		csts 15855	. . . 4 class sSet
16	8, 14, 15	co 6650	. . 3 class ( (toInc ` ( CSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. )
17	2, 3, 16	cmpt 4729	. 2 class ( h e. _V |-> ( (toInc ` ( CSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. ) )
18	1, 17	wceq 1483	1 wff toHL = ( h e. _V |-> ( (toInc ` ( CSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. ) )

This definition is referenced by:  thlval  20039