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

Theorem latmcom 14181
Description: The join of a lattice commutes. (incom 3361 analog.) (Contributed by NM, 6-Nov-2011.)
Hypotheses
Ref Expression
latmcom.b  |-  B  =  ( Base `  K
)
latmcom.m  |-  ./\  =  ( meet `  K )
Assertion
Ref Expression
latmcom  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  =  ( Y 
./\  X ) )

Proof of Theorem latmcom
StepHypRef Expression
1 latmcom.b . . . 4  |-  B  =  ( Base `  K
)
2 latmcom.m . . . 4  |-  ./\  =  ( meet `  K )
31, 2latmcl 14157 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  e.  B )
41, 2latmcl 14157 . . . 4  |-  ( ( K  e.  Lat  /\  Y  e.  B  /\  X  e.  B )  ->  ( Y  ./\  X
)  e.  B )
543com23 1157 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( Y  ./\  X
)  e.  B )
63, 5jca 518 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( ( X  ./\  Y )  e.  B  /\  ( Y  ./\  X )  e.  B ) )
7 latpos 14155 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
81, 2meetcom 14138 . . 3  |-  ( ( ( K  e.  Poset  /\  X  e.  B  /\  Y  e.  B )  /\  ( ( X  ./\  Y )  e.  B  /\  ( Y  ./\  X )  e.  B ) )  ->  ( X  ./\  Y )  =  ( Y 
./\  X ) )
97, 8syl3anl1 1230 . 2  |-  ( ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  /\  ( ( X  ./\  Y )  e.  B  /\  ( Y  ./\  X )  e.  B ) )  ->  ( X  ./\  Y )  =  ( Y 
./\  X ) )
106, 9mpdan 649 1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  =  ( Y 
./\  X ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   ` cfv 5255  (class class class)co 5858   Basecbs 13148   Posetcpo 14074   meetcmee 14079   Latclat 14151
This theorem is referenced by:  latleeqm2  14186  latmlem2  14188  latmlej21  14198  latmlej22  14199  mod2ile  14212  olm12  29418  latm12  29420  latm32  29421  latmrot  29422  olm02  29427  omllaw2N  29434  cmtcomlemN  29438  cmtbr3N  29444  omlfh1N  29448  omlmod1i2N  29450  omlspjN  29451  cvlcvrp  29530  intnatN  29596  cvrexch  29609  cvrat4  29632  2atjm  29634  1cvrat  29665  2at0mat0  29714  dalem4  29854  dalem56  29917  atmod2i1  30050  atmod2i2  30051  llnmod2i2  30052  atmod3i1  30053  atmod3i2  30054  llnexchb2lem  30057  dalawlem3  30062  dalawlem4  30063  dalawlem6  30065  dalawlem9  30068  dalawlem11  30070  dalawlem12  30071  dalawlem15  30074  lhpmcvr  30212  4atexlemc  30258  cdleme20zN  30490  cdleme20d  30501  cdleme20l  30511  cdleme20m  30512  cdlemg12  30839  cdlemg17  30866  cdlemg19  30873  cdlemg44a  30920  dihmeetlem17N  31513  dihmeetlem20N  31516  dihmeetALTN  31517
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-meet 14111  df-lat 14152
  Copyright terms: Public domain W3C validator