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 𝐾 = ( toHL ‘ 𝑊 )
thloc.c = ( ocv ‘ 𝑊 )
Assertion thloc = ( oc ‘ 𝐾 )

Proof

Step Hyp Ref Expression
1 thlval.k 𝐾 = ( toHL ‘ 𝑊 )
2 thloc.c = ( ocv ‘ 𝑊 )
3 fvex ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) ∈ V
4 2 fvexi ∈ V
5 ocid oc = Slot ( oc ‘ ndx )
6 5 setsid ( ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) ∈ V ∧ ∈ V ) → = ( oc ‘ ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet ⟨ ( oc ‘ ndx ) , ⟩ ) ) )
7 3 4 6 mp2an = ( oc ‘ ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet ⟨ ( oc ‘ ndx ) , ⟩ ) )
8 eqid ( ClSubSp ‘ 𝑊 ) = ( ClSubSp ‘ 𝑊 )
9 eqid ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) = ( toInc ‘ ( ClSubSp ‘ 𝑊 ) )
10 1 8 9 2 thlval ( 𝑊 ∈ V → 𝐾 = ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet ⟨ ( oc ‘ ndx ) , ⟩ ) )
11 10 fveq2d ( 𝑊 ∈ V → ( oc ‘ 𝐾 ) = ( oc ‘ ( ( toInc ‘ ( ClSubSp ‘ 𝑊 ) ) sSet ⟨ ( oc ‘ ndx ) , ⟩ ) ) )
12 7 11 eqtr4id ( 𝑊 ∈ V → = ( oc ‘ 𝐾 ) )
13 5 str0 ∅ = ( oc ‘ ∅ )
14 fvprc ( ¬ 𝑊 ∈ V → ( ocv ‘ 𝑊 ) = ∅ )
15 2 14 syl5eq ( ¬ 𝑊 ∈ V → = ∅ )
16 fvprc ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
17 1 16 syl5eq ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
18 17 fveq2d ( ¬ 𝑊 ∈ V → ( oc ‘ 𝐾 ) = ( oc ‘ ∅ ) )
19 13 15 18 3eqtr4a ( ¬ 𝑊 ∈ V → = ( oc ‘ 𝐾 ) )
20 12 19 pm2.61i = ( oc ‘ 𝐾 )