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		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
6	1 2 3 5	thlval	$$⊢W\in \mathrm{V}\to K=I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩$$
7	6	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)}$$
8		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
9		10re	$$⊢10\in ℝ$$
10		1nn0	$$⊢1\in {\mathbb{N}}_0$$
11		0nn0	$$⊢0\in {\mathbb{N}}_0$$
12		1nn	$$⊢1\in \mathbb{N}$$
13		0lt1	$$⊢0<1$$
14	10 11 12 13	declt	$$⊢10<11$$
15	9 14	ltneii	$$⊢10\ne 11$$
16		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
17		ocndx	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)=11$$
18	16 17	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 11$$
19	15 18	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)$$
20	8 19	setsnid	$$⊢{\le }_I={\le }_{\left(I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
21	4 20	eqtri	$$⊢\underset{\dot{}}{\le }={\le }_{\left(I\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
22	7 21	syl6reqr	$$⊢W\in \mathrm{V}\to \underset{\dot{}}{\le }={\le }_K$$
23	8	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	syl5eq	$$⊢\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	syl5eq	$$⊢\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$$