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

Metamath Proof Explorer

Theorem thlle

Description: Ordering on 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 )
thlle.i 
|- I = ( toInc ` C )
thlle.l 
|- .<_ = ( le ` I )
Assertion thlle 
|- .<_ = ( 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 plendxnocndx 
 |-  ( le ` ndx ) =/= ( oc ` ndx )
7 5 6 setsnid 
 |-  ( le ` I ) = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
8 4 7 eqtri 
 |-  .<_ = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
9 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
10 1 2 3 9 thlval 
 |-  ( W e. _V -> K = ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
11 10 fveq2d 
 |-  ( W e. _V -> ( le ` K ) = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) ) )
12 8 11 eqtr4id 
 |-  ( W e. _V -> .<_ = ( le ` K ) )
13 5 str0 
 |-  (/) = ( le ` (/) )
14 2 fvexi 
 |-  C e. _V
15 3 ipolerval 
 |-  ( C e. _V -> { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = ( le ` I ) )
16 14 15 ax-mp 
 |-  { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = ( le ` I )
17 4 16 eqtr4i 
 |-  .<_ = { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) }
18 opabn0 
 |-  ( { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } =/= (/) <-> E. x E. y ( { x , y } C_ C /\ x C_ y ) )
19 vex 
 |-  x e. _V
20 vex 
 |-  y e. _V
21 19 20 prss 
 |-  ( ( x e. C /\ y e. C ) <-> { x , y } C_ C )
22 elfvex 
 |-  ( x e. ( ClSubSp ` W ) -> W e. _V )
23 22 2 eleq2s 
 |-  ( x e. C -> W e. _V )
24 23 ad2antrr 
 |-  ( ( ( x e. C /\ y e. C ) /\ x C_ y ) -> W e. _V )
25 21 24 sylanbr 
 |-  ( ( { x , y } C_ C /\ x C_ y ) -> W e. _V )
26 25 exlimivv 
 |-  ( E. x E. y ( { x , y } C_ C /\ x C_ y ) -> W e. _V )
27 18 26 sylbi 
 |-  ( { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } =/= (/) -> W e. _V )
28 27 necon1bi 
 |-  ( -. W e. _V -> { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = (/) )
29 17 28 eqtrid 
 |-  ( -. W e. _V -> .<_ = (/) )
30 fvprc 
 |-  ( -. W e. _V -> ( toHL ` W ) = (/) )
31 1 30 eqtrid 
 |-  ( -. W e. _V -> K = (/) )
32 31 fveq2d 
 |-  ( -. W e. _V -> ( le ` K ) = ( le ` (/) ) )
33 13 29 32 3eqtr4a 
 |-  ( -. W e. _V -> .<_ = ( le ` K ) )
34 12 33 pm2.61i 
 |-  .<_ = ( le ` K )