Theorem thlbas

Description: Base set of 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)$$
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		basendxnocndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{oc}\left(\mathrm{ndx}\right)$$
9	7 8	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)}$$
10	6 9	eqtri	$$⊢C={\mathrm{Base}}_{\left(\mathrm{toInc}\left(C\right)\mathrm{sSet}⟨\mathrm{oc}\left(\mathrm{ndx}\right),\mathrm{ocv}\left(W\right)⟩\right)}$$
11		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
12	1 2 4 11	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)⟩$$
13	12	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)}$$
14	10 13	eqtr4id	$$⊢W\in \mathrm{V}\to C={\mathrm{Base}}_K$$
15		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
16		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{ClSubSp}\left(W\right)=\varnothing$$
17	2 16	eqtrid	$$⊢\neg W\in \mathrm{V}\to C=\varnothing$$
18		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{toHL}\left(W\right)=\varnothing$$
19	1 18	eqtrid	$$⊢\neg W\in \mathrm{V}\to K=\varnothing$$
20	19	fveq2d	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_K={\mathrm{Base}}_{\varnothing }$$
21	15 17 20	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to C={\mathrm{Base}}_K$$
22	14 21	pm2.61i	$$⊢C={\mathrm{Base}}_K$$