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

Theorem latjcom 16260
Description: The join of a lattice commutes. (chjcom 27002 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 4886 . . . . 5  |-  ( ( X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e.  ( B  X.  B
) )
213adant1 1023 . . . 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 2429 . . . . . . 7  |-  ( meet `  K )  =  (
meet `  K )
63, 4, 5islat 16248 . . . . . 6  |-  ( K  e.  Lat  <->  ( K  e.  Poset  /\  ( dom  .\/  =  ( B  X.  B )  /\  dom  ( meet `  K )  =  ( B  X.  B ) ) ) )
7 simprl 762 . . . . . 6  |-  ( ( K  e.  Poset  /\  ( dom  .\/  =  ( B  X.  B )  /\  dom  ( meet `  K
)  =  ( B  X.  B ) ) )  ->  dom  .\/  =  ( B  X.  B
) )
86, 7sylbi 198 . . . . 5  |-  ( K  e.  Lat  ->  dom  .\/  =  ( B  X.  B ) )
983ad2ant1 1026 . . . 4  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  dom  .\/  =  ( B  X.  B ) )
102, 9eleqtrrd 2520 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e. 
dom  .\/  )
11 opelxpi 4886 . . . . . 6  |-  ( ( Y  e.  B  /\  X  e.  B )  -> 
<. Y ,  X >.  e.  ( B  X.  B
) )
1211ancoms 454 . . . . 5  |-  ( ( X  e.  B  /\  Y  e.  B )  -> 
<. Y ,  X >.  e.  ( B  X.  B
) )
13123adant1 1023 . . . 4  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. Y ,  X >.  e.  ( B  X.  B
) )
1413, 9eleqtrrd 2520 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. Y ,  X >.  e. 
dom  .\/  )
1510, 14jca 534 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( <. X ,  Y >.  e.  dom  .\/  /\  <. Y ,  X >.  e. 
dom  .\/  ) )
16 latpos 16251 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
173, 4joincom 16231 . . 3  |-  ( ( ( K  e.  Poset  /\  X  e.  B  /\  Y  e.  B )  /\  ( <. X ,  Y >.  e.  dom  .\/  /\  <. Y ,  X >.  e. 
dom  .\/  ) )  -> 
( X  .\/  Y
)  =  ( Y 
.\/  X ) )
1816, 17syl3anl1 1312 . 2  |-  ( ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  /\  ( <. X ,  Y >.  e.  dom  .\/  /\  <. Y ,  X >.  e. 
dom  .\/  ) )  -> 
( X  .\/  Y
)  =  ( Y 
.\/  X ) )
1915, 18mpdan 672 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 370    /\ w3a 982    = wceq 1437    e. wcel 1870   <.cop 4008    X. cxp 4852   dom cdm 4854   ` cfv 5601  (class class class)co 6305   Basecbs 15084   Posetcpo 16140   joincjn 16144   meetcmee 16145   Latclat 16246
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  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 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  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-lub 16175  df-join 16177  df-lat 16247
This theorem is referenced by:  latleeqj2  16265  latjlej2  16267  latnle  16286  latmlej12  16292  latj12  16297  latj32  16298  latj13  16299  latj31  16300  latj4rot  16303  mod2ile  16307  latdisdlem  16390  olj02  32512  omllaw4  32532  cmt2N  32536  cmtbr3N  32540  cvlexch2  32615  cvlexchb2  32617  cvlatexchb2  32621  cvlatexch2  32623  cvlatexch3  32624  cvlatcvr2  32628  cvlsupr2  32629  cvlsupr7  32634  cvlsupr8  32635  hlatjcom  32653  hlrelat5N  32686  cvrval5  32700  cvrexch  32705  cvratlem  32706  cvrat  32707  2atlt  32724  cvrat3  32727  cvrat4  32728  cvrat42  32729  4noncolr3  32738  1cvrat  32761  3atlem1  32768  4atlem4d  32887  4atlem12  32897  paddcom  33098  paddasslem2  33106  pmapjat2  33139  atmod2i1  33146  atmod2i2  33147  llnmod2i2  33148  atmod4i1  33151  atmod4i2  33152  dalawlem4  33159  dalawlem9  33164  dalawlem12  33167  lhpjat2  33306  lhple  33327  trljat1  33452  trljat2  33453  cdlemc1  33477  cdlemc6  33482  cdlemd1  33484  cdleme5  33526  cdleme9  33539  cdleme10  33540  cdleme19e  33594  trlcolem  34013  trljco2  34028  cdlemk7  34135  cdlemk7u  34157  cdlemkid1  34209  dih1  34574  dihjatc2N  34600
  Copyright terms: Public domain W3C validator