| 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
|
eqtrid |
|- ( W e. _V -> K = ( I sSet <. ( oc ` ndx ) , ._|_ >. ) ) |
| 18 |
5 17
|
syl |
|- ( W e. V -> K = ( I sSet <. ( oc ` ndx ) , ._|_ >. ) ) |