Theorem thlle

Description: Ordering 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)$$
	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		10re	$$⊢10\in ℝ$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		0nn0	$$⊢0\in {\mathbb{N}}_0$$
9		1nn	$$⊢1\in \mathbb{N}$$
10		0lt1	$$⊢0<1$$
11	7 8 9 10	declt	$$⊢10<11$$
12	6 11	ltneii	$$⊢10\ne 11$$
13		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
14		ocndx	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)=11$$
15	13 14	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 11$$
16	12 15	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)$$
17	5 16	setsnid	$$⊢{\le }_I={\le }_{\left(I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
18	4 17	eqtri	$$⊢\underset{\dot{}}{\le }={\le }_{\left(I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
19		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
20	1 2 3 19	thlval	$$⊢W\in \mathrm{V}\to K=I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩$$
21	20	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)}$$
22	18 21	eqtr4id	$$⊢W\in \mathrm{V}\to \underset{\dot{}}{\le }={\le }_K$$
23	5	str0	$$⊢\varnothing ={\le }_{\varnothing }$$
24	2	fvexi	$$⊢C\in \mathrm{V}$$
25	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$$
26	24 25	ax-mp	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}={\le }_I$$
27	4 26	eqtr4i	$$⊢\underset{\dot{}}{\le }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}$$
28		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)$$
29		vex	$$⊢x\in \mathrm{V}$$
30		vex	$$⊢y\in \mathrm{V}$$
31	29 30	prss	$$⊢\left(x\in C\wedge y\in C\right)\leftrightarrow \left\{x,y\right\}\subseteq C$$
32		elfvex	$$⊢x\in \mathrm{ClSubSp}\left(W\right)\to W\in \mathrm{V}$$
33	32 2	eleq2s	$$⊢x\in C\to W\in \mathrm{V}$$
34	33	ad2antrr	$$⊢\left(\left(x\in C\wedge y\in C\right)\wedge x\subseteq y\right)\to W\in \mathrm{V}$$
35	31 34	sylanbr	$$⊢\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\to W\in \mathrm{V}$$
36	35	exlimivv	$$⊢\exists x\exists y\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\to W\in \mathrm{V}$$
37	28 36	sylbi	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}\ne \varnothing \to W\in \mathrm{V}$$
38	37	necon1bi	$$⊢\neg W\in \mathrm{V}\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq C\wedge x\subseteq y\right)\right\}=\varnothing$$
39	27 38	eqtrid	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\le }=\varnothing$$
40		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{toHL}\left(W\right)=\varnothing$$
41	1 40	eqtrid	$$⊢\neg W\in \mathrm{V}\to K=\varnothing$$
42	41	fveq2d	$$⊢\neg W\in \mathrm{V}\to {\le }_K={\le }_{\varnothing }$$
43	23 39 42	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\le }={\le }_K$$
44	22 43	pm2.61i	$$⊢\underset{\dot{}}{\le }={\le }_K$$