Theorem thloc

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

	Ref	Expression
Hypotheses	thlval.k	$$⊢K=\mathrm{toHL}\left(W\right)$$
	thloc.c	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
Assertion	thloc	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$

Proof

Step	Hyp	Ref	Expression
1		thlval.k	$$⊢K=\mathrm{toHL}\left(W\right)$$
2		thloc.c	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
3		fvex	$$⊢\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)\in \mathrm{V}$$
4	2	fvexi	$$⊢\underset{\dot{}}{\perp }\in \mathrm{V}$$
5		ocid	$$⊢\mathrm{oc}=\mathrm{Slot}\mathrm{oc}\left(\mathrm{ndx}\right)$$
6	5	setsid	$$⊢\left(\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)\in \mathrm{V}\wedge \underset{\dot{}}{\perp }\in \mathrm{V}\right)\to \underset{\dot{}}{\perp }=\mathrm{oc}\left(\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\underset{\dot{}}{\perp }⟩\right)$$
7	3 4 6	mp2an	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\underset{\dot{}}{\perp }⟩\right)$$
8		eqid	$$⊢\mathrm{ClSubSp}\left(W\right)=\mathrm{ClSubSp}\left(W\right)$$
9		eqid	$$⊢\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)=\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)$$
10	1 8 9 2	thlval	$$⊢W\in \mathrm{V}\to K=\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\underset{\dot{}}{\perp }⟩$$
11	10	fveq2d	$$⊢W\in \mathrm{V}\to \mathrm{oc}\left(K\right)=\mathrm{oc}\left(\mathrm{toInc}\left(\mathrm{ClSubSp}\left(W\right)\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\underset{\dot{}}{\perp }⟩\right)$$
12	7 11	eqtr4id	$$⊢W\in \mathrm{V}\to \underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
13	5	str0	$$⊢\varnothing =\mathrm{oc}\left(\varnothing \right)$$
14		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{ocv}\left(W\right)=\varnothing$$
15	2 14	syl5eq	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }=\varnothing$$
16		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{toHL}\left(W\right)=\varnothing$$
17	1 16	syl5eq	$$⊢\neg W\in \mathrm{V}\to K=\varnothing$$
18	17	fveq2d	$$⊢\neg W\in \mathrm{V}\to \mathrm{oc}\left(K\right)=\mathrm{oc}\left(\varnothing \right)$$
19	13 15 18	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
20	12 19	pm2.61i	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$