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

Theorem ishlat2 34025
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 34024 . 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 33995 . . . . 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 1184 . . . 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 649 . . . . 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 970 . . . . . 6  |-  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat )  <->  ( ( K  e.  OML  /\  K  e.  CLat )  /\  K  e.  AtLat ) )
1312anbi1i 695 . . . . 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 970 . . . . 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 278 . . . 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 249 . . 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 695 . 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 649 . . 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 649 . . . . 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 450 . . . . . . 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 2983 . . . . . . 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 252 . . . . . 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 695 . . . . 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 251 . . . 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 694 . . 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 249 . 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 271 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 968    = wceq 1374    e. wcel 1762    =/= wne 2655   A.wral 2807   E.wrex 2808   class class class wbr 4440   ` cfv 5579  (class class class)co 6275   Basecbs 14479   lecple 14551   ltcplt 15417   joincjn 15420   0.cp0 15513   1.cp1 15514   CLatccla 15583   OMLcoml 33847   Atomscatm 33935   AtLatcal 33936   CvLatclc 33937   HLchlt 34022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-cvlat 33994  df-hlat 34023
This theorem is referenced by:  ishlatiN  34027  hlsuprexch  34052  hlhgt4  34059
  Copyright terms: Public domain W3C validator