Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ishlat2 Unicode version

Theorem ishlat2 29602
Description: The predicate "is a Hilbert lattice". Here we replace  K  e.  CvLat with the weaker  K  e.  AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012.)
Hypotheses
Ref Expression
ishlat.b  |-  B  =  ( Base `  K
)
ishlat.l  |-  .<_  =  ( le `  K )
ishlat.s  |-  .<  =  ( lt `  K )
ishlat.j  |-  .\/  =  ( join `  K )
ishlat.z  |-  .0.  =  ( 0. `  K )
ishlat.u  |-  .1.  =  ( 1. `  K )
ishlat.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
ishlat2  |-  ( K  e.  HL  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )
Distinct variable groups:    x, y,
z, A    x, B, y, z    x, K, y, z
Allowed substitution hints:    .< ( x, y,
z)    .1. ( x, y, z)    .\/ ( x, y, z)    .<_ ( x, y, z)    .0. ( x, y, z)

Proof of Theorem ishlat2
StepHypRef Expression
1 ishlat.b . . 3  |-  B  =  ( Base `  K
)
2 ishlat.l . . 3  |-  .<_  =  ( le `  K )
3 ishlat.s . . 3  |-  .<  =  ( lt `  K )
4 ishlat.j . . 3  |-  .\/  =  ( join `  K )
5 ishlat.z . . 3  |-  .0.  =  ( 0. `  K )
6 ishlat.u . . 3  |-  .1.  =  ( 1. `  K )
7 ishlat.a . . 3  |-  A  =  ( Atoms `  K )
81, 2, 3, 4, 5, 6, 7ishlat1 29601 . 2  |-  ( K  e.  HL  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat
)  /\  ( A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )
91, 2, 4, 7iscvlat 29572 . . . . 5  |-  ( K  e.  CvLat 
<->  ( K  e.  AtLat  /\ 
A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  ->  y  .<_  ( z  .\/  x ) ) ) )
1093anbi3i 1145 . . . 4  |-  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat )  <->  ( K  e.  OML  /\  K  e. 
CLat  /\  ( K  e. 
AtLat  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) ) ) )
11 anass 630 . . . . 5  |-  ( ( ( ( K  e. 
OML  /\  K  e.  CLat )  /\  K  e. 
AtLat )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  <-> 
( ( K  e. 
OML  /\  K  e.  CLat )  /\  ( K  e.  AtLat  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) ) ) )
12 df-3an 937 . . . . . 6  |-  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat )  <->  ( ( K  e.  OML  /\  K  e.  CLat )  /\  K  e.  AtLat ) )
1312anbi1i 676 . . . . 5  |-  ( ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) )  <->  ( ( ( K  e.  OML  /\  K  e.  CLat )  /\  K  e.  AtLat )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) ) )
14 df-3an 937 . . . . 5  |-  ( ( K  e.  OML  /\  K  e.  CLat  /\  ( K  e.  AtLat  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) ) )  <->  ( ( K  e.  OML  /\  K  e.  CLat )  /\  ( K  e.  AtLat  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) ) ) )
1511, 13, 143bitr4ri 269 . . . 4  |-  ( ( K  e.  OML  /\  K  e.  CLat  /\  ( K  e.  AtLat  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) ) )  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) ) )
1610, 15bitri 240 . . 3  |-  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat )  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) ) )
1716anbi1i 676 . 2  |-  ( ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat )  /\  ( A. x  e.  A  A. y  e.  A  ( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) )  <->  ( ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) )  /\  ( A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )
18 anass 630 . . 3  |-  ( ( ( ( K  e. 
OML  /\  K  e.  CLat  /\  K  e.  AtLat )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) )  /\  ( A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) )  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  ( A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) )  /\  ( A. x  e.  A  A. y  e.  A  ( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x  .\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  (
(  .0.  .<  x  /\  x  .<  y )  /\  ( y  .< 
z  /\  z  .<  .1.  ) ) ) ) ) )
19 anass 630 . . . . 5  |-  ( ( ( A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) )  /\  A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  (
(  .0.  .<  x  /\  x  .<  y )  /\  ( y  .< 
z  /\  z  .<  .1.  ) ) )  <->  ( A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) )  /\  ( A. x  e.  A  A. y  e.  A  ( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x  .\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  (
(  .0.  .<  x  /\  x  .<  y )  /\  ( y  .< 
z  /\  z  .<  .1.  ) ) ) ) )
20 ancom 437 . . . . . . 7  |-  ( ( A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  ->  y  .<_  ( z  .\/  x ) )  /\  A. x  e.  A  A. y  e.  A  ( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x  .\/  y ) ) ) )  <->  ( A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) ) )
21 r19.26-2 2761 . . . . . . 7  |-  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  <-> 
( A. x  e.  A  A. y  e.  A  ( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x  .\/  y ) ) )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) ) )
2220, 21bitr4i 243 . . . . . 6  |-  ( ( A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  ->  y  .<_  ( z  .\/  x ) )  /\  A. x  e.  A  A. y  e.  A  ( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x  .\/  y ) ) ) )  <->  A. x  e.  A  A. y  e.  A  ( (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) ) )
2322anbi1i 676 . . . . 5  |-  ( ( ( A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) )  /\  A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  (
(  .0.  .<  x  /\  x  .<  y )  /\  ( y  .< 
z  /\  z  .<  .1.  ) ) )  <->  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) )
2419, 23bitr3i 242 . . . 4  |-  ( ( A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  ->  y  .<_  ( z  .\/  x ) )  /\  ( A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) )  <->  ( A. x  e.  A  A. y  e.  A  ( (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) )
2524anbi2i 675 . . 3  |-  ( ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat )  /\  ( A. x  e.  A  A. y  e.  A  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  ->  y  .<_  ( z  .\/  x ) )  /\  ( A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )
2618, 25bitri 240 . 2  |-  ( ( ( ( K  e. 
OML  /\  K  e.  CLat  /\  K  e.  AtLat )  /\  A. x  e.  A  A. y  e.  A  A. z  e.  B  (
( -.  x  .<_  z  /\  x  .<_  ( z 
.\/  y ) )  ->  y  .<_  ( z 
.\/  x ) ) )  /\  ( A. x  e.  A  A. y  e.  A  (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) )  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )
278, 17, 263bitri 262 1  |-  ( K  e.  HL  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 935    = wceq 1647    e. wcel 1715    =/= wne 2529   A.wral 2628   E.wrex 2629   class class class wbr 4125   ` cfv 5358  (class class class)co 5981   Basecbs 13356   lecple 13423   ltcplt 14285   joincjn 14288   0.cp0 14353   1.cp1 14354   CLatccla 14423   OMLcoml 29424   Atomscatm 29512   AtLatcal 29513   CvLatclc 29514   HLchlt 29599
This theorem is referenced by:  ishlatiN  29604  hlsuprexch  29629  hlhgt4  29636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984  df-cvlat 29571  df-hlat 29600
  Copyright terms: Public domain W3C validator