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 )