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 = ( toHL ` W )
	thlbas.c	|- C = ( ClSubSp ` W )
Assertion	thlbas	|- C = ( Base ` K )

Proof

Step	Hyp	Ref	Expression
1		thlval.k	|- K = ( toHL ` W )
2		thlbas.c	|- C = ( ClSubSp ` W )
3	2	fvexi	|- C e. _V
4		eqid	|- ( toInc ` C ) = ( toInc ` C )
5	4	ipobas	|- ( C e. _V -> C = ( Base ` ( toInc ` C ) ) )
6	3 5	ax-mp	|- C = ( Base ` ( toInc ` C ) )
7		baseid	|- Base = Slot ( Base ` ndx )
8		basendxnocndx	|- ( Base ` ndx ) =/= ( oc ` ndx )
9	7 8	setsnid	|- ( Base ` ( toInc ` C ) ) = ( Base ` ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
10	6 9	eqtri	|- C = ( Base ` ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
11		eqid	|- ( ocv ` W ) = ( ocv ` W )
12	1 2 4 11	thlval	|- ( W e. _V -> K = ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
13	12	fveq2d	|- ( W e. _V -> ( Base ` K ) = ( Base ` ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) ) )
14	10 13	eqtr4id	|- ( W e. _V -> C = ( Base ` K ) )
15		base0	|- (/) = ( Base ` (/) )
16		fvprc	|- ( -. W e. _V -> ( ClSubSp ` W ) = (/) )
17	2 16	eqtrid	|- ( -. W e. _V -> C = (/) )
18		fvprc	|- ( -. W e. _V -> ( toHL ` W ) = (/) )
19	1 18	eqtrid	|- ( -. W e. _V -> K = (/) )
20	19	fveq2d	|- ( -. W e. _V -> ( Base ` K ) = ( Base ` (/) ) )
21	15 17 20	3eqtr4a	|- ( -. W e. _V -> C = ( Base ` K ) )
22	14 21	pm2.61i	|- C = ( Base ` K )