Theorem thlle

Description: Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015) (Proof shortened by AV, 11-Nov-2024)

	Ref	Expression
Hypotheses	thlval.k	$$⊢K=\mathrm{toHL}\left(W\right)$$
	thlbas.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
	thlle.i	$$⊢I=\mathrm{toInc}\left(C\right)$$
	thlle.l	$$⊢\underset{\dot{}}{\le }={\le }_I$$
Assertion	thlle	$$⊢\underset{\dot{}}{\le }={\le }_K$$

Proof

Step	Hyp	Ref	Expression
1		thlval.k	$$⊢K=\mathrm{toHL}\left(W\right)$$
2		thlbas.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
3		thlle.i	$$⊢I=\mathrm{toInc}\left(C\right)$$
4		thlle.l	$$⊢\underset{\dot{}}{\le }={\le }_I$$
5		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
6		plendxnocndx	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)$$
7	5 6	setsnid	$$⊢{\le }_I={\le }_{\left(I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
8	4 7	eqtri	$$⊢\underset{\dot{}}{\le }={\le }_{\left(I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
9		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
10	1 2 3 9	thlval	$$⊢W\in \mathrm{V}\to K=I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩$$
11	10	fveq2d	$$⊢W\in \mathrm{V}\to {\le }_K={\le }_{\left(I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
12	8 11	eqtr4id	$$⊢W\in \mathrm{V}\to \underset{\dot{}}{\le }={\le }_K$$
13	5	str0	$$⊢\varnothing ={\le }_{\varnothing }$$
14	2	fvexi	$$⊢C\in \mathrm{V}$$
15	3	ipolerval	$$⊢C\in \mathrm{V}\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}={\le }_I$$
16	14 15	ax-mp	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}={\le }_I$$
17	4 16	eqtr4i	$$⊢\underset{\dot{}}{\le }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}$$
18		opabn0	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}\ne \varnothing \leftrightarrow \exists x\exists y\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)$$
19		vex	$$⊢x\in \mathrm{V}$$
20		vex	$$⊢y\in \mathrm{V}$$
21	19 20	prss	$$⊢\left(x\in C\wedge y\in C\right)\leftrightarrow \left\{x,y\right\}\subseteq C$$
22		elfvex	$$⊢x\in \mathrm{ClSubSp}\left(W\right)\to W\in \mathrm{V}$$
23	22 2	eleq2s	$$⊢x\in C\to W\in \mathrm{V}$$
24	23	ad2antrr	$$⊢\left(\left(x\in C\wedge y\in C\right)\wedge x\subseteq y\right)\to W\in \mathrm{V}$$
25	21 24	sylanbr	$$⊢\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\to W\in \mathrm{V}$$
26	25	exlimivv	$$⊢\exists x\exists y\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\to W\in \mathrm{V}$$
27	18 26	sylbi	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}\ne \varnothing \to W\in \mathrm{V}$$
28	27	necon1bi	$$⊢\neg W\in \mathrm{V}\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}=\varnothing$$
29	17 28	eqtrid	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\le }=\varnothing$$
30		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{toHL}\left(W\right)=\varnothing$$
31	1 30	eqtrid	$$⊢\neg W\in \mathrm{V}\to K=\varnothing$$
32	31	fveq2d	$$⊢\neg W\in \mathrm{V}\to {\le }_K={\le }_{\varnothing }$$
33	13 29 32	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\le }={\le }_K$$
34	12 33	pm2.61i	$$⊢\underset{\dot{}}{\le }={\le }_K$$