Theorem thlval

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

	Ref	Expression
Hypotheses	thlval.k	|- K = ( toHL ` W )
	thlval.c	|- C = ( ClSubSp ` W )
	thlval.i	|- I = ( toInc ` C )
	thlval.o	|- ._|_ = ( ocv ` W )
Assertion	thlval	|- ( W e. V -> K = ( I sSet <. ( oc ` ndx ) , ._|_ >. ) )

Proof

Step	Hyp	Ref	Expression
1		thlval.k	|- K = ( toHL ` W )
2		thlval.c	|- C = ( ClSubSp ` W )
3		thlval.i	|- I = ( toInc ` C )
4		thlval.o	|- ._|_ = ( ocv ` W )
5		elex	|- ( W e. V -> W e. _V )
6		fveq2	|- ( h = W -> ( ClSubSp ` h ) = ( ClSubSp ` W ) )
7	6 2	eqtr4di	|- ( h = W -> ( ClSubSp ` h ) = C )
8	7	fveq2d	|- ( h = W -> ( toInc ` ( ClSubSp ` h ) ) = ( toInc ` C ) )
9	8 3	eqtr4di	|- ( h = W -> ( toInc ` ( ClSubSp ` h ) ) = I )
10		fveq2	|- ( h = W -> ( ocv ` h ) = ( ocv ` W ) )
11	10 4	eqtr4di	|- ( h = W -> ( ocv ` h ) = ._|_ )
12	11	opeq2d	|- ( h = W -> <. ( oc ` ndx ) , ( ocv ` h ) >. = <. ( oc ` ndx ) , ._|_ >. )
13	9 12	oveq12d	|- ( h = W -> ( ( toInc ` ( ClSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. ) = ( I sSet <. ( oc ` ndx ) , ._|_ >. ) )
14		df-thl	|- toHL = ( h e. _V |-> ( ( toInc ` ( ClSubSp ` h ) ) sSet <. ( oc ` ndx ) , ( ocv ` h ) >. ) )
15		ovex	|- ( I sSet <. ( oc ` ndx ) , ._|_ >. ) e. _V
16	13 14 15	fvmpt	|- ( W e. _V -> ( toHL ` W ) = ( I sSet <. ( oc ` ndx ) , ._|_ >. ) )
17	1 16	syl5eq	|- ( W e. _V -> K = ( I sSet <. ( oc ` ndx ) , ._|_ >. ) )
18	5 17	syl	|- ( W e. V -> K = ( I sSet <. ( oc ` ndx ) , ._|_ >. ) )