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 = ( 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		1re	|- 1 e. RR
9		1nn	|- 1 e. NN
10		1nn0	|- 1 e. NN0
11		1lt10	|- 1 < ; 1 0
12	9 10 10 11	declti	|- 1 < ; 1 1
13	8 12	ltneii	|- 1 =/= ; 1 1
14		basendx	|- ( Base ` ndx ) = 1
15		ocndx	|- ( oc ` ndx ) = ; 1 1
16	14 15	neeq12i	|- ( ( Base ` ndx ) =/= ( oc ` ndx ) <-> 1 =/= ; 1 1 )
17	13 16	mpbir	|- ( Base ` ndx ) =/= ( oc ` ndx )
18	7 17	setsnid	|- ( Base ` ( toInc ` C ) ) = ( Base ` ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
19	6 18	eqtri	|- C = ( Base ` ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
20		eqid	|- ( ocv ` W ) = ( ocv ` W )
21	1 2 4 20	thlval	|- ( W e. _V -> K = ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
22	21	fveq2d	|- ( W e. _V -> ( Base ` K ) = ( Base ` ( ( toInc ` C ) sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) ) )
23	19 22	eqtr4id	|- ( W e. _V -> C = ( Base ` K ) )
24		base0	|- (/) = ( Base ` (/) )
25		fvprc	|- ( -. W e. _V -> ( ClSubSp ` W ) = (/) )
26	2 25	eqtrid	|- ( -. W e. _V -> C = (/) )
27		fvprc	|- ( -. W e. _V -> ( toHL ` W ) = (/) )
28	1 27	eqtrid	|- ( -. W e. _V -> K = (/) )
29	28	fveq2d	|- ( -. W e. _V -> ( Base ` K ) = ( Base ` (/) ) )
30	24 26 29	3eqtr4a	|- ( -. W e. _V -> C = ( Base ` K ) )
31	23 30	pm2.61i	|- C = ( Base ` K )