Metamath Proof Explorer

Theorem thlleOLD

Description: Obsolete proof of thlle as of 11-Nov-2024. Ordering on 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 )
thlle.i 
|- I = ( toInc ` C )
thlle.l 
|- .<_ = ( le ` I )
Assertion thlleOLD 
|- .<_ = ( le ` K )

Proof

Step Hyp Ref Expression
1 thlval.k 
 |-  K = ( toHL ` W )
2 thlbas.c 
 |-  C = ( ClSubSp ` W )
3 thlle.i 
 |-  I = ( toInc ` C )
4 thlle.l 
 |-  .<_ = ( le ` I )
5 pleid 
 |-  le = Slot ( le ` ndx )
6 10re 
 |-  ; 1 0 e. RR
7 1nn0 
 |-  1 e. NN0
8 0nn0 
 |-  0 e. NN0
9 1nn 
 |-  1 e. NN
10 0lt1 
 |-  0 < 1
11 7 8 9 10 declt 
 |-  ; 1 0 < ; 1 1
12 6 11 ltneii 
 |-  ; 1 0 =/= ; 1 1
13 plendx 
 |-  ( le ` ndx ) = ; 1 0
14 ocndx 
 |-  ( oc ` ndx ) = ; 1 1
15 13 14 neeq12i 
 |-  ( ( le ` ndx ) =/= ( oc ` ndx ) <-> ; 1 0 =/= ; 1 1 )
16 12 15 mpbir 
 |-  ( le ` ndx ) =/= ( oc ` ndx )
17 5 16 setsnid 
 |-  ( le ` I ) = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
18 4 17 eqtri 
 |-  .<_ = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
19 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
20 1 2 3 19 thlval 
 |-  ( W e. _V -> K = ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
21 20 fveq2d 
 |-  ( W e. _V -> ( le ` K ) = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) ) )
22 18 21 eqtr4id 
 |-  ( W e. _V -> .<_ = ( le ` K ) )
23 5 str0 
 |-  (/) = ( le ` (/) )
24 2 fvexi 
 |-  C e. _V
25 3 ipolerval 
 |-  ( C e. _V -> { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = ( le ` I ) )
26 24 25 ax-mp 
 |-  { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = ( le ` I )
27 4 26 eqtr4i 
 |-  .<_ = { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) }
28 opabn0 
 |-  ( { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } =/= (/) <-> E. x E. y ( { x , y } C_ C /\ x C_ y ) )
29 vex 
 |-  x e. _V
30 vex 
 |-  y e. _V
31 29 30 prss 
 |-  ( ( x e. C /\ y e. C ) <-> { x , y } C_ C )
32 elfvex 
 |-  ( x e. ( ClSubSp ` W ) -> W e. _V )
33 32 2 eleq2s 
 |-  ( x e. C -> W e. _V )
34 33 ad2antrr 
 |-  ( ( ( x e. C /\ y e. C ) /\ x C_ y ) -> W e. _V )
35 31 34 sylanbr 
 |-  ( ( { x , y } C_ C /\ x C_ y ) -> W e. _V )
36 35 exlimivv 
 |-  ( E. x E. y ( { x , y } C_ C /\ x C_ y ) -> W e. _V )
37 28 36 sylbi 
 |-  ( { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } =/= (/) -> W e. _V )
38 37 necon1bi 
 |-  ( -. W e. _V -> { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = (/) )
39 27 38 eqtrid 
 |-  ( -. W e. _V -> .<_ = (/) )
40 fvprc 
 |-  ( -. W e. _V -> ( toHL ` W ) = (/) )
41 1 40 eqtrid 
 |-  ( -. W e. _V -> K = (/) )
42 41 fveq2d 
 |-  ( -. W e. _V -> ( le ` K ) = ( le ` (/) ) )
43 23 39 42 3eqtr4a 
 |-  ( -. W e. _V -> .<_ = ( le ` K ) )
44 22 43 pm2.61i 
 |-  .<_ = ( le ` K )