Metamath Proof Explorer

Theorem thloc

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

Ref Expression
Hypotheses thlval.k 
|- K = ( toHL ` W )
thloc.c 
|- ._|_ = ( ocv ` W )
Assertion thloc 
|- ._|_ = ( oc ` K )

Proof

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 )