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 ‘ 𝐾 )