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