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

Theorem latmcom 15245
Description: The join of a lattice commutes. (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 opelxpi 4871 . . . . 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 latmcom.b . . . . . . 7  |-  B  =  ( Base `  K
)
4 eqid 2443 . . . . . . 7  |-  ( join `  K )  =  (
join `  K )
5 latmcom.m . . . . . . 7  |-  ./\  =  ( meet `  K )
63, 4, 5islat 15217 . . . . . 6  |-  ( K  e.  Lat  <->  ( K  e.  Poset  /\  ( dom  ( join `  K )  =  ( B  X.  B )  /\  dom  ./\  =  ( B  X.  B ) ) ) )
7 simprr 756 . . . . . 6  |-  ( ( K  e.  Poset  /\  ( dom  ( join `  K
)  =  ( B  X.  B )  /\  dom  ./\  =  ( 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 2520 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e. 
dom  ./\  )
11 opelxpi 4871 . . . . . 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 2520 . . 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 15220 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
173, 5meetcom 15202 . . 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 3883    X. cxp 4838   dom cdm 4840   ` cfv 5418  (class class class)co 6091   Basecbs 14174   Posetcpo 15110   joincjn 15114   meetcmee 15115   Latclat 15215
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 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
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 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-glb 15145  df-meet 15147  df-lat 15216
This theorem is referenced by:  latleeqm2  15250  latmlem2  15252  latmlej21  15262  latmlej22  15263  mod2ile  15276  olm12  32873  latm12  32875  latm32  32876  latmrot  32877  olm02  32882  omllaw2N  32889  cmtcomlemN  32893  cmtbr3N  32899  omlfh1N  32903  omlmod1i2N  32905  omlspjN  32906  cvlcvrp  32985  intnatN  33051  cvrexch  33064  cvrat4  33087  2atjm  33089  1cvrat  33120  2at0mat0  33169  dalem4  33309  dalem56  33372  atmod2i1  33505  atmod2i2  33506  llnmod2i2  33507  atmod3i1  33508  atmod3i2  33509  llnexchb2lem  33512  dalawlem3  33517  dalawlem4  33518  dalawlem6  33520  dalawlem9  33523  dalawlem11  33525  dalawlem12  33526  dalawlem15  33529  lhpmcvr  33667  4atexlemc  33713  cdleme20zN  33945  cdleme20d  33956  cdleme20l  33966  cdleme20m  33967  cdlemg12  34294  cdlemg17  34321  cdlemg19  34328  cdlemg44a  34375  dihmeetlem17N  34968  dihmeetlem20N  34971  dihmeetALTN  34972
  Copyright terms: Public domain W3C validator