This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )