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

Theorem latjcom 15351
Description: The join of a lattice commutes. (chjcom 25081 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 4982 . . . . 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 2454 . . . . . . 7  |-  ( meet `  K )  =  (
meet `  K )
63, 4, 5islat 15339 . . . . . 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 2545 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e. 
dom  .\/  )
11 opelxpi 4982 . . . . . 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 2545 . . 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 15342 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
173, 4joincom 15322 . . 3  |-  ( ( ( K  e.  Poset  /\  X  e.  B  /\  Y  e.  B )  /\  ( <. X ,  Y >.  e.  dom  .\/  /\  <. Y ,  X >.  e. 
dom  .\/  ) )  -> 
( X  .\/  Y
)  =  ( Y 
.\/  X ) )
1816, 17syl3anl1 1267 . 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 1370    e. wcel 1758   <.cop 3994    X. cxp 4949   dom cdm 4951   ` cfv 5529  (class class class)co 6203   Basecbs 14295   Posetcpo 15232   joincjn 15236   meetcmee 15237   Latclat 15337
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-riota 6164  df-ov 6206  df-oprab 6207  df-lub 15266  df-join 15268  df-lat 15338
This theorem is referenced by:  latleeqj2  15356  latjlej2  15358  latnle  15377  latmlej12  15383  latj12  15388  latj32  15389  latj13  15390  latj31  15391  latj4rot  15394  mod2ile  15398  latdisdlem  15481  olj02  33229  omllaw4  33249  cmt2N  33253  cmtbr3N  33257  cvlexch2  33332  cvlexchb2  33334  cvlatexchb2  33338  cvlatexch2  33340  cvlatexch3  33341  cvlatcvr2  33345  cvlsupr2  33346  cvlsupr7  33351  cvlsupr8  33352  hlatjcom  33370  hlrelat5N  33403  cvrval5  33417  cvrexch  33422  cvratlem  33423  cvrat  33424  2atlt  33441  cvrat3  33444  cvrat4  33445  cvrat42  33446  4noncolr3  33455  1cvrat  33478  3atlem1  33485  4atlem4d  33604  4atlem12  33614  paddcom  33815  paddasslem2  33823  pmapjat2  33856  atmod2i1  33863  atmod2i2  33864  llnmod2i2  33865  atmod4i1  33868  atmod4i2  33869  dalawlem4  33876  dalawlem9  33881  dalawlem12  33884  lhpjat2  34023  lhple  34044  trljat1  34168  trljat2  34169  cdlemc1  34193  cdlemc6  34198  cdlemd1  34200  cdleme5  34242  cdleme9  34255  cdleme10  34256  cdleme19e  34309  trlcolem  34728  trljco2  34743  cdlemk7  34850  cdlemk7u  34872  cdlemkid1  34924  dih1  35289  dihjatc2N  35315
  Copyright terms: Public domain W3C validator