MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latjcom Structured version   Unicode version

Theorem latjcom 15221
Description: The join of a lattice commutes. (chjcom 24860 analog.) (Contributed by NM, 16-Sep-2011.)
Hypotheses
Ref Expression
latjcom.b  |-  B  =  ( Base `  K
)
latjcom.j  |-  .\/  =  ( join `  K )
Assertion
Ref Expression
latjcom  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  =  ( Y 
.\/  X ) )

Proof of Theorem latjcom
StepHypRef Expression
1 opelxpi 4866 . . . . 5  |-  ( ( X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e.  ( B  X.  B
) )
213adant1 1006 . . . 4  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e.  ( B  X.  B
) )
3 latjcom.b . . . . . . 7  |-  B  =  ( Base `  K
)
4 latjcom.j . . . . . . 7  |-  .\/  =  ( join `  K )
5 eqid 2438 . . . . . . 7  |-  ( meet `  K )  =  (
meet `  K )
63, 4, 5islat 15209 . . . . . 6  |-  ( K  e.  Lat  <->  ( K  e.  Poset  /\  ( dom  .\/  =  ( B  X.  B )  /\  dom  ( meet `  K )  =  ( B  X.  B ) ) ) )
7 simprl 755 . . . . . 6  |-  ( ( K  e.  Poset  /\  ( dom  .\/  =  ( B  X.  B )  /\  dom  ( meet `  K
)  =  ( B  X.  B ) ) )  ->  dom  .\/  =  ( B  X.  B
) )
86, 7sylbi 195 . . . . 5  |-  ( K  e.  Lat  ->  dom  .\/  =  ( B  X.  B ) )
983ad2ant1 1009 . . . 4  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  dom  .\/  =  ( B  X.  B ) )
102, 9eleqtrrd 2515 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e. 
dom  .\/  )
11 opelxpi 4866 . . . . . 6  |-  ( ( Y  e.  B  /\  X  e.  B )  -> 
<. Y ,  X >.  e.  ( B  X.  B
) )
1211ancoms 453 . . . . 5  |-  ( ( X  e.  B  /\  Y  e.  B )  -> 
<. Y ,  X >.  e.  ( B  X.  B
) )
13123adant1 1006 . . . 4  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. Y ,  X >.  e.  ( B  X.  B
) )
1413, 9eleqtrrd 2515 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. Y ,  X >.  e. 
dom  .\/  )
1510, 14jca 532 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( <. X ,  Y >.  e.  dom  .\/  /\  <. Y ,  X >.  e. 
dom  .\/  ) )
16 latpos 15212 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
173, 4joincom 15192 . . 3  |-  ( ( ( K  e.  Poset  /\  X  e.  B  /\  Y  e.  B )  /\  ( <. X ,  Y >.  e.  dom  .\/  /\  <. Y ,  X >.  e. 
dom  .\/  ) )  -> 
( X  .\/  Y
)  =  ( Y 
.\/  X ) )
1816, 17syl3anl1 1266 . 2  |-  ( ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  /\  ( <. X ,  Y >.  e.  dom  .\/  /\  <. Y ,  X >.  e. 
dom  .\/  ) )  -> 
( X  .\/  Y
)  =  ( Y 
.\/  X ) )
1915, 18mpdan 668 1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  =  ( Y 
.\/  X ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   <.cop 3878    X. cxp 4833   dom cdm 4835   ` cfv 5413  (class class class)co 6086   Basecbs 14166   Posetcpo 15102   joincjn 15106   meetcmee 15107   Latclat 15207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-lub 15136  df-join 15138  df-lat 15208
This theorem is referenced by:  latleeqj2  15226  latjlej2  15228  latnle  15247  latmlej12  15253  latj12  15258  latj32  15259  latj13  15260  latj31  15261  latj4rot  15264  mod2ile  15268  latdisdlem  15351  olj02  32711  omllaw4  32731  cmt2N  32735  cmtbr3N  32739  cvlexch2  32814  cvlexchb2  32816  cvlatexchb2  32820  cvlatexch2  32822  cvlatexch3  32823  cvlatcvr2  32827  cvlsupr2  32828  cvlsupr7  32833  cvlsupr8  32834  hlatjcom  32852  hlrelat5N  32885  cvrval5  32899  cvrexch  32904  cvratlem  32905  cvrat  32906  2atlt  32923  cvrat3  32926  cvrat4  32927  cvrat42  32928  4noncolr3  32937  1cvrat  32960  3atlem1  32967  4atlem4d  33086  4atlem12  33096  paddcom  33297  paddasslem2  33305  pmapjat2  33338  atmod2i1  33345  atmod2i2  33346  llnmod2i2  33347  atmod4i1  33350  atmod4i2  33351  dalawlem4  33358  dalawlem9  33363  dalawlem12  33366  lhpjat2  33505  lhple  33526  trljat1  33650  trljat2  33651  cdlemc1  33675  cdlemc6  33680  cdlemd1  33682  cdleme5  33724  cdleme9  33737  cdleme10  33738  cdleme19e  33791  trlcolem  34210  trljco2  34225  cdlemk7  34332  cdlemk7u  34354  cdlemkid1  34406  dih1  34771  dihjatc2N  34797
  Copyright terms: Public domain W3C validator