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

Theorem atnle 32852
Description: Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 28027 analog.) (Contributed by NM, 5-Nov-2012.)
Hypotheses
Ref Expression
atnle.b  |-  B  =  ( Base `  K
)
atnle.l  |-  .<_  =  ( le `  K )
atnle.m  |-  ./\  =  ( meet `  K )
atnle.z  |-  .0.  =  ( 0. `  K )
atnle.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
atnle  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  ( -.  P  .<_  X  <->  ( P  ./\ 
X )  =  .0.  ) )

Proof of Theorem atnle
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 simpl1 1008 . . . . . 6  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =/=  .0.  )  ->  K  e.  AtLat )
2 atllat 32835 . . . . . . . . 9  |-  ( K  e.  AtLat  ->  K  e.  Lat )
323ad2ant1 1026 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  K  e.  Lat )
4 atnle.b . . . . . . . . . 10  |-  B  =  ( Base `  K
)
5 atnle.a . . . . . . . . . 10  |-  A  =  ( Atoms `  K )
64, 5atbase 32824 . . . . . . . . 9  |-  ( P  e.  A  ->  P  e.  B )
763ad2ant2 1027 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  P  e.  B )
8 simp3 1007 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  X  e.  B )
9 atnle.m . . . . . . . . 9  |-  ./\  =  ( meet `  K )
104, 9latmcl 16297 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  P  e.  B  /\  X  e.  B )  ->  ( P  ./\  X
)  e.  B )
113, 7, 8, 10syl3anc 1264 . . . . . . 7  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  ( P  ./\  X )  e.  B )
1211adantr 466 . . . . . 6  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =/=  .0.  )  ->  ( P  ./\  X
)  e.  B )
13 simpr 462 . . . . . 6  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =/=  .0.  )  ->  ( P  ./\  X
)  =/=  .0.  )
14 atnle.l . . . . . . 7  |-  .<_  =  ( le `  K )
15 atnle.z . . . . . . 7  |-  .0.  =  ( 0. `  K )
164, 14, 15, 5atlex 32851 . . . . . 6  |-  ( ( K  e.  AtLat  /\  ( P  ./\  X )  e.  B  /\  ( P 
./\  X )  =/= 
.0.  )  ->  E. y  e.  A  y  .<_  ( P  ./\  X )
)
171, 12, 13, 16syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =/=  .0.  )  ->  E. y  e.  A  y  .<_  ( P  ./\  X ) )
18 simpl1 1008 . . . . . . . . . 10  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  K  e.  AtLat
)
1918, 2syl 17 . . . . . . . . 9  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  K  e.  Lat )
204, 5atbase 32824 . . . . . . . . . 10  |-  ( y  e.  A  ->  y  e.  B )
2120adantl 467 . . . . . . . . 9  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  y  e.  B )
22 simpl2 1009 . . . . . . . . . 10  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  P  e.  A )
2322, 6syl 17 . . . . . . . . 9  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  P  e.  B )
24 simpl3 1010 . . . . . . . . 9  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  X  e.  B )
254, 14, 9latlem12 16323 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  ( y  e.  B  /\  P  e.  B  /\  X  e.  B
) )  ->  (
( y  .<_  P  /\  y  .<_  X )  <->  y  .<_  ( P  ./\  X )
) )
2619, 21, 23, 24, 25syl13anc 1266 . . . . . . . 8  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  ( (
y  .<_  P  /\  y  .<_  X )  <->  y  .<_  ( P  ./\  X )
) )
27 simpr 462 . . . . . . . . . . 11  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  y  e.  A )
2814, 5atcmp 32846 . . . . . . . . . . 11  |-  ( ( K  e.  AtLat  /\  y  e.  A  /\  P  e.  A )  ->  (
y  .<_  P  <->  y  =  P ) )
2918, 27, 22, 28syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  ( y  .<_  P  <->  y  =  P ) )
30 breq1 4426 . . . . . . . . . . 11  |-  ( y  =  P  ->  (
y  .<_  X  <->  P  .<_  X ) )
3130biimpd 210 . . . . . . . . . 10  |-  ( y  =  P  ->  (
y  .<_  X  ->  P  .<_  X ) )
3229, 31syl6bi 231 . . . . . . . . 9  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  ( y  .<_  P  ->  ( y  .<_  X  ->  P  .<_  X ) ) )
3332impd 432 . . . . . . . 8  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  ( (
y  .<_  P  /\  y  .<_  X )  ->  P  .<_  X ) )
3426, 33sylbird 238 . . . . . . 7  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  y  e.  A
)  ->  ( y  .<_  ( P  ./\  X
)  ->  P  .<_  X ) )
3534adantlr 719 . . . . . 6  |-  ( ( ( ( K  e. 
AtLat  /\  P  e.  A  /\  X  e.  B
)  /\  ( P  ./\ 
X )  =/=  .0.  )  /\  y  e.  A
)  ->  ( y  .<_  ( P  ./\  X
)  ->  P  .<_  X ) )
3635rexlimdva 2914 . . . . 5  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =/=  .0.  )  ->  ( E. y  e.  A  y  .<_  ( P 
./\  X )  ->  P  .<_  X ) )
3717, 36mpd 15 . . . 4  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =/=  .0.  )  ->  P  .<_  X )
3837ex 435 . . 3  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  (
( P  ./\  X
)  =/=  .0.  ->  P 
.<_  X ) )
3938necon1bd 2638 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  ( -.  P  .<_  X  -> 
( P  ./\  X
)  =  .0.  )
)
4015, 5atn0 32843 . . . 4  |-  ( ( K  e.  AtLat  /\  P  e.  A )  ->  P  =/=  .0.  )
41403adant3 1025 . . 3  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  P  =/=  .0.  )
424, 14, 9latleeqm1 16324 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  P  e.  B  /\  X  e.  B )  ->  ( P  .<_  X  <->  ( P  ./\ 
X )  =  P ) )
433, 7, 8, 42syl3anc 1264 . . . . . . 7  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  ( P  .<_  X  <->  ( P  ./\ 
X )  =  P ) )
4443adantr 466 . . . . . 6  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =  .0.  )  ->  ( P  .<_  X  <->  ( P  ./\ 
X )  =  P ) )
45 eqeq1 2426 . . . . . . . 8  |-  ( ( P  ./\  X )  =  P  ->  ( ( P  ./\  X )  =  .0.  <->  P  =  .0.  ) )
4645biimpcd 227 . . . . . . 7  |-  ( ( P  ./\  X )  =  .0.  ->  ( ( P  ./\  X )  =  P  ->  P  =  .0.  ) )
4746adantl 467 . . . . . 6  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =  .0.  )  ->  ( ( P  ./\  X )  =  P  ->  P  =  .0.  )
)
4844, 47sylbid 218 . . . . 5  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =  .0.  )  ->  ( P  .<_  X  ->  P  =  .0.  )
)
4948necon3ad 2630 . . . 4  |-  ( ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  /\  ( P  ./\  X
)  =  .0.  )  ->  ( P  =/=  .0.  ->  -.  P  .<_  X ) )
5049ex 435 . . 3  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  (
( P  ./\  X
)  =  .0.  ->  ( P  =/=  .0.  ->  -.  P  .<_  X )
) )
5141, 50mpid 42 . 2  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  (
( P  ./\  X
)  =  .0.  ->  -.  P  .<_  X )
)
5239, 51impbid 193 1  |-  ( ( K  e.  AtLat  /\  P  e.  A  /\  X  e.  B )  ->  ( -.  P  .<_  X  <->  ( P  ./\ 
X )  =  .0.  ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872    =/= wne 2614   E.wrex 2772   class class class wbr 4423   ` cfv 5601  (class class class)co 6305   Basecbs 15120   lecple 15196   meetcmee 16189   0.cp0 16282   Latclat 16290   Atomscatm 32798   AtLatcal 32799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-preset 16172  df-poset 16190  df-plt 16203  df-lub 16219  df-glb 16220  df-join 16221  df-meet 16222  df-p0 16284  df-lat 16291  df-covers 32801  df-ats 32802  df-atl 32833
This theorem is referenced by:  atnem0  32853  iscvlat2N  32859  cvlexch3  32867  cvlexch4N  32868  cvlcvrp  32875  intnatN  32941  cvrat4  32977  dalem24  33231  cdlema2N  33326  llnexchb2lem  33402  lhpmat  33564  ltrnmwOLD  33686  cdleme15b  33810  cdlemednpq  33834  cdleme20zN  33836  cdleme20yOLD  33838  cdleme22cN  33878  dihmeetlem7N  34847  dihmeetlem17N  34860
  Copyright terms: Public domain W3C validator