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

Theorem latmcom 18352
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 5670 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
213adant1 1130 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
3 latmcom.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 eqid 2736 . . . . . . 7 (join‘𝐾) = (join‘𝐾)
5 latmcom.m . . . . . . 7 = (meet‘𝐾)
63, 4, 5islat 18322 . . . . . 6 (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom (join‘𝐾) = (𝐵 × 𝐵) ∧ dom = (𝐵 × 𝐵))))
7 simprr 771 . . . . . 6 ((𝐾 ∈ Poset ∧ (dom (join‘𝐾) = (𝐵 × 𝐵) ∧ dom = (𝐵 × 𝐵))) → dom = (𝐵 × 𝐵))
86, 7sylbi 216 . . . . 5 (𝐾 ∈ Lat → dom = (𝐵 × 𝐵))
983ad2ant1 1133 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → dom = (𝐵 × 𝐵))
102, 9eleqtrrd 2841 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
11 opelxpi 5670 . . . . . 6 ((𝑌𝐵𝑋𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1211ancoms 459 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
13123adant1 1130 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ (𝐵 × 𝐵))
1413, 9eleqtrrd 2841 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑌, 𝑋⟩ ∈ dom )
1510, 14jca 512 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom ))
16 latpos 18327 . . 3 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
173, 5meetcom 18293 . . 3 (((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1816, 17syl3anl1 1412 . 2 (((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑌, 𝑋⟩ ∈ dom )) → (𝑋 𝑌) = (𝑌 𝑋))
1915, 18mpdan 685 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑌 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  cop 4592   × cxp 5631  dom cdm 5633  cfv 6496  (class class class)co 7357  Basecbs 17083  Posetcpo 18196  joincjn 18200  meetcmee 18201  Latclat 18320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-glb 18236  df-meet 18238  df-lat 18321
This theorem is referenced by:  latleeqm2  18357  latmlem2  18359  latmlej21  18369  latmlej22  18370  mod2ile  18383  olm12  37690  latm12  37692  latm32  37693  latmrot  37694  olm02  37699  omllaw2N  37706  cmtcomlemN  37710  cmtbr3N  37716  omlfh1N  37720  omlmod1i2N  37722  omlspjN  37723  cvlcvrp  37802  intnatN  37870  cvrexch  37883  cvrat4  37906  2atjm  37908  1cvrat  37939  2at0mat0  37988  dalem4  38128  dalem56  38191  atmod2i1  38324  atmod2i2  38325  llnmod2i2  38326  atmod3i1  38327  atmod3i2  38328  llnexchb2lem  38331  dalawlem3  38336  dalawlem4  38337  dalawlem6  38339  dalawlem9  38342  dalawlem11  38344  dalawlem12  38345  dalawlem15  38348  lhpmcvr  38486  4atexlemc  38532  cdleme20zN  38764  cdleme20d  38775  cdleme20l  38785  cdleme20m  38786  cdlemg12  39113  cdlemg17  39140  cdlemg19  39147  cdlemg44a  39194  dihmeetlem17N  39786  dihmeetlem20N  39789  dihmeetALTN  39790
  Copyright terms: Public domain W3C validator