Metamath Proof Explorer

Theorem thlbasOLD

Description: Obsolete proof of thlbas as of 11-Nov-2024. Base set of the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses thlval.k 
|- K = ( toHL ` W )
thlbas.c 
|- C = ( ClSubSp ` W )
Assertion thlbasOLD 
|- 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 )