Step |
Hyp |
Ref |
Expression |
1 |
|
thlval.k |
|- K = ( toHL ` W ) |
2 |
|
thloc.c |
|- ._|_ = ( ocv ` W ) |
3 |
|
fvex |
|- ( toInc ` ( ClSubSp ` W ) ) e. _V |
4 |
2
|
fvexi |
|- ._|_ e. _V |
5 |
|
ocid |
|- oc = Slot ( oc ` ndx ) |
6 |
5
|
setsid |
|- ( ( ( toInc ` ( ClSubSp ` W ) ) e. _V /\ ._|_ e. _V ) -> ._|_ = ( oc ` ( ( toInc ` ( ClSubSp ` W ) ) sSet <. ( oc ` ndx ) , ._|_ >. ) ) ) |
7 |
3 4 6
|
mp2an |
|- ._|_ = ( oc ` ( ( toInc ` ( ClSubSp ` W ) ) sSet <. ( oc ` ndx ) , ._|_ >. ) ) |
8 |
|
eqid |
|- ( ClSubSp ` W ) = ( ClSubSp ` W ) |
9 |
|
eqid |
|- ( toInc ` ( ClSubSp ` W ) ) = ( toInc ` ( ClSubSp ` W ) ) |
10 |
1 8 9 2
|
thlval |
|- ( W e. _V -> K = ( ( toInc ` ( ClSubSp ` W ) ) sSet <. ( oc ` ndx ) , ._|_ >. ) ) |
11 |
10
|
fveq2d |
|- ( W e. _V -> ( oc ` K ) = ( oc ` ( ( toInc ` ( ClSubSp ` W ) ) sSet <. ( oc ` ndx ) , ._|_ >. ) ) ) |
12 |
7 11
|
eqtr4id |
|- ( W e. _V -> ._|_ = ( oc ` K ) ) |
13 |
5
|
str0 |
|- (/) = ( oc ` (/) ) |
14 |
|
fvprc |
|- ( -. W e. _V -> ( ocv ` W ) = (/) ) |
15 |
2 14
|
syl5eq |
|- ( -. W e. _V -> ._|_ = (/) ) |
16 |
|
fvprc |
|- ( -. W e. _V -> ( toHL ` W ) = (/) ) |
17 |
1 16
|
syl5eq |
|- ( -. W e. _V -> K = (/) ) |
18 |
17
|
fveq2d |
|- ( -. W e. _V -> ( oc ` K ) = ( oc ` (/) ) ) |
19 |
13 15 18
|
3eqtr4a |
|- ( -. W e. _V -> ._|_ = ( oc ` K ) ) |
20 |
12 19
|
pm2.61i |
|- ._|_ = ( oc ` K ) |