Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlatjcom Structured version   Visualization version   GIF version

Theorem hlatjcom 35256
Description: Commutatitivity of join operation. Frequently-used special case of latjcom 17326 for atoms. (Contributed by NM, 15-Jun-2012.)
Hypotheses
Ref Expression
hlatjcom.j = (join‘𝐾)
hlatjcom.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
hlatjcom ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) = (𝑌 𝑋))

Proof of Theorem hlatjcom
StepHypRef Expression
1 hllat 35251 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 eqid 2764 . . 3 (Base‘𝐾) = (Base‘𝐾)
3 hlatjcom.a . . 3 𝐴 = (Atoms‘𝐾)
42, 3atbase 35177 . 2 (𝑋𝐴𝑋 ∈ (Base‘𝐾))
52, 3atbase 35177 . 2 (𝑌𝐴𝑌 ∈ (Base‘𝐾))
6 hlatjcom.j . . 3 = (join‘𝐾)
72, 6latjcom 17326 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 𝑌) = (𝑌 𝑋))
81, 4, 5, 7syl3an 1199 1 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 𝑌) = (𝑌 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107   = wceq 1652  wcel 2155  cfv 6067  (class class class)co 6841  Basecbs 16131  joincjn 17211  Latclat 17312  Atomscatm 35151  HLchlt 35238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-lub 17241  df-join 17243  df-lat 17313  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239
This theorem is referenced by:  hlatj12  35259  hlatjrot  35261  hlatlej2  35264  atbtwnex  35336  3noncolr2  35337  hlatcon2  35340  3dimlem2  35347  3dimlem3  35349  3dimlem3OLDN  35350  3dimlem4  35352  3dimlem4OLDN  35353  ps-1  35365  hlatexch4  35369  lplnribN  35439  4atlem10  35494  4atlem11  35497  dalemswapyz  35544  dalem-cly  35559  dalemswapyzps  35578  dalem24  35585  dalem25  35586  dalem44  35604  2llnma1  35675  2llnma3r  35676  2llnma2rN  35678  llnexchb2  35757  dalawlem4  35762  dalawlem5  35763  dalawlem9  35767  dalawlem11  35769  dalawlem12  35770  dalawlem15  35773  4atexlemex2  35959  4atexlemcnd  35960  ltrncnv  36034  trlcnv  36053  cdlemc6  36084  cdleme7aa  36130  cdleme12  36159  cdleme15a  36162  cdleme15c  36164  cdleme17c  36176  cdlemeda  36186  cdleme19a  36191  cdleme19e  36195  cdleme20bN  36198  cdleme20g  36203  cdleme20m  36211  cdleme21c  36215  cdleme22f  36234  cdleme22g  36236  cdleme35b  36338  cdleme35f  36342  cdleme37m  36350  cdleme39a  36353  cdleme42h  36370  cdleme43aN  36377  cdleme43bN  36378  cdleme43dN  36380  cdleme46f2g2  36381  cdleme46f2g1  36382  cdlemeg46c  36401  cdlemeg46nlpq  36405  cdlemeg46ngfr  36406  cdlemeg46rgv  36416  cdlemeg46gfv  36418  cdlemg2kq  36490  cdlemg4a  36496  cdlemg4d  36501  cdlemg4  36505  cdlemg8c  36517  cdlemg11aq  36526  cdlemg10a  36528  cdlemg12g  36537  cdlemg12  36538  cdlemg13  36540  cdlemg17pq  36560  cdlemg18b  36567  cdlemg18c  36568  cdlemg19  36572  cdlemg21  36574  cdlemk7  36736  cdlemk7u  36758  cdlemkfid1N  36809  dia2dimlem1  36952  dia2dimlem3  36954  dihjatcclem3  37308  dihjat  37311
  Copyright terms: Public domain W3C validator