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

Theorem latmcom 17272
Description: The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.)
Hypotheses
Ref Expression
latmcom.b 𝐵 = (Base‘𝐾)
latmcom.m = (meet‘𝐾)
Assertion
Ref Expression
latmcom ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑌 𝑋))

Proof of Theorem latmcom
StepHypRef Expression
1 opelxpi 5301 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
213adant1 1125 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
3 latmcom.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 eqid 2756 . . . . . . 7 (join‘𝐾) = (join‘𝐾)
5 latmcom.m . . . . . . 7 = (meet‘𝐾)
63, 4, 5islat 17244 . . . . . 6 (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom (join‘𝐾) = (𝐵 × 𝐵) ∧ dom = (𝐵 × 𝐵))))
7 simprr 813 . . . . . 6 ((𝐾 ∈ Poset ∧ (dom (join‘𝐾) = (𝐵 × 𝐵) ∧ dom = (𝐵 × 𝐵))) → dom = (𝐵 × 𝐵))
86, 7sylbi 207 . . . . 5 (𝐾 ∈ Lat → dom = (𝐵 × 𝐵))
983ad2ant1 1128 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → dom = (𝐵 × 𝐵))
102, 9eleqtrrd 2838 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
11 opelxpi 5301 . . . . . 6 ((𝑌𝐵𝑋𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1211ancoms 468 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
13123adant1 1125 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1413, 9eleqtrrd 2838 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ dom )
1510, 14jca 555 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom ))
16 latpos 17247 . . 3 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
173, 5meetcom 17229 . . 3 (((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1816, 17syl3anl1 1521 . 2 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1915, 18mpdan 705 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑌 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1628  wcel 2135  cop 4323   × cxp 5260  dom cdm 5262  cfv 6045  (class class class)co 6809  Basecbs 16055  Posetcpo 17137  joincjn 17141  meetcmee 17142  Latclat 17242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-glb 17172  df-meet 17174  df-lat 17243
This theorem is referenced by:  latleeqm2  17277  latmlem2  17279  latmlej21  17289  latmlej22  17290  mod2ile  17303  olm12  35014  latm12  35016  latm32  35017  latmrot  35018  olm02  35023  omllaw2N  35030  cmtcomlemN  35034  cmtbr3N  35040  omlfh1N  35044  omlmod1i2N  35046  omlspjN  35047  cvlcvrp  35126  intnatN  35192  cvrexch  35205  cvrat4  35228  2atjm  35230  1cvrat  35261  2at0mat0  35310  dalem4  35450  dalem56  35513  atmod2i1  35646  atmod2i2  35647  llnmod2i2  35648  atmod3i1  35649  atmod3i2  35650  llnexchb2lem  35653  dalawlem3  35658  dalawlem4  35659  dalawlem6  35661  dalawlem9  35664  dalawlem11  35666  dalawlem12  35667  dalawlem15  35670  lhpmcvr  35808  4atexlemc  35854  cdleme20zN  36087  cdleme20d  36098  cdleme20l  36108  cdleme20m  36109  cdlemg12  36436  cdlemg17  36463  cdlemg19  36470  cdlemg44a  36517  dihmeetlem17N  37110  dihmeetlem20N  37113  dihmeetALTN  37114
  Copyright terms: Public domain W3C validator