Theorem thlbas

Description: Base set of 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)$$
Assertion	thlbas	$$⊢C={\mathrm{Base}}_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	2	fvexi	$$⊢C\in \mathrm{V}$$
4		eqid	$$⊢\mathrm{toInc}\left(C\right)=\mathrm{toInc}\left(C\right)$$
5	4	ipobas	$$⊢C\in \mathrm{V}\to C={\mathrm{Base}}_{\mathrm{toInc}\left(C\right)}$$
6	3 5	ax-mp	$$⊢C={\mathrm{Base}}_{\mathrm{toInc}\left(C\right)}$$
7		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
8		1re	$$⊢1\in ℝ$$
9		1nn	$$⊢1\in \mathbb{N}$$
10		1nn0	$$⊢1\in {\mathbb{N}}_0$$
11		1lt10	$$⊢1<10$$
12	9 10 10 11	declti	$$⊢1<11$$
13	8 12	ltneii	$$⊢1\ne 11$$
14		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
15		ocndx	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)=11$$
16	14 15	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 11$$
17	13 16	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)$$
18	7 17	setsnid	$$⊢{\mathrm{Base}}_{\mathrm{toInc}\left(C\right)}={\mathrm{Base}}_{\left(\mathrm{toInc}\left(C\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
19	6 18	eqtri	$$⊢C={\mathrm{Base}}_{\left(\mathrm{toInc}\left(C\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
20		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
21	1 2 4 20	thlval	$$⊢W\in \mathrm{V}\to K=\mathrm{toInc}\left(C\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩$$
22	21	fveq2d	$$⊢W\in \mathrm{V}\to {\mathrm{Base}}_K={\mathrm{Base}}_{\left(\mathrm{toInc}\left(C\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
23	19 22	eqtr4id	$$⊢W\in \mathrm{V}\to C={\mathrm{Base}}_K$$
24		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
25		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{ClSubSp}\left(W\right)=\varnothing$$
26	2 25	syl5eq	$$⊢\neg W\in \mathrm{V}\to C=\varnothing$$
27		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{toHL}\left(W\right)=\varnothing$$
28	1 27	syl5eq	$$⊢\neg W\in \mathrm{V}\to K=\varnothing$$
29	28	fveq2d	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_K={\mathrm{Base}}_{\varnothing }$$
30	24 26 29	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to C={\mathrm{Base}}_K$$
31	23 30	pm2.61i	$$⊢C={\mathrm{Base}}_K$$