This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ¬ 𝑊 ∈ V → ⊥ = ∅ )
16 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( toHL ‘ 𝑊 ) = ∅ )
17 1 16 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝐾 = ∅ )
18 17 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( oc ‘ 𝐾 ) = ( oc ‘ ∅ ) )
19 13 15 18 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → ⊥ = ( oc ‘ 𝐾 ) )
20 12 19 pm2.61i ⊢ ⊥ = ( oc ‘ 𝐾 )