Theorem hlatjcom 38834

Description: Commutatitivity of join operation. Frequently-used special case of latjcom 18432 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

Step	Hyp	Ref	Expression
1		hllat 38829	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		eqid 2728	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		hlatjcom.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 38755	. 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ (Base‘𝐾))
5	2, 3	atbase 38755	. 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ (Base‘𝐾))
6		hlatjcom.j	. . 3 ⊢ ∨ = (join‘𝐾)
7	2, 6	latjcom 18432	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
8	1, 4, 5, 7	syl3an 1158	1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ‘cfv 6542  (class class class)co 7414  Basecbs 17173  joincjn 18296  Latclat 18416  Atomscatm 38729  HLchlt 38816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-lub 18331  df-join 18333  df-lat 18417  df-ats 38733  df-atl 38764  df-cvlat 38788  df-hlat 38817

This theorem is referenced by:  hlatj12  38837  hlatjrot  38839  hlatlej2  38842  atbtwnex  38915  3noncolr2  38916  hlatcon2  38919  3dimlem2  38926  3dimlem3  38928  3dimlem3OLDN  38929  3dimlem4  38931  3dimlem4OLDN  38932  ps-1  38944  hlatexch4  38948  lplnribN  39018  4atlem10  39073  4atlem11  39076  dalemswapyz  39123  dalem-cly  39138  dalemswapyzps  39157  dalem24  39164  dalem25  39165  dalem44  39183  2llnma1  39254  2llnma3r  39255  2llnma2rN  39257  llnexchb2  39336  dalawlem4  39341  dalawlem5  39342  dalawlem9  39346  dalawlem11  39348  dalawlem12  39349  dalawlem15  39352  4atexlemex2  39538  4atexlemcnd  39539  ltrncnv  39613  trlcnv  39632  cdlemc6  39663  cdleme7aa  39709  cdleme12  39738  cdleme15a  39741  cdleme15c  39743  cdleme17c  39755  cdlemeda  39765  cdleme19a  39770  cdleme19e  39774  cdleme20bN  39777  cdleme20g  39782  cdleme20m  39790  cdleme21c  39794  cdleme22f  39813  cdleme22g  39815  cdleme35b  39917  cdleme35f  39921  cdleme37m  39929  cdleme39a  39932  cdleme42h  39949  cdleme43aN  39956  cdleme43bN  39957  cdleme43dN  39959  cdleme46f2g2  39960  cdleme46f2g1  39961  cdlemeg46c  39980  cdlemeg46nlpq  39984  cdlemeg46ngfr  39985  cdlemeg46rgv  39995  cdlemeg46gfv  39997  cdlemg2kq  40069  cdlemg4a  40075  cdlemg4d  40080  cdlemg4  40084  cdlemg8c  40096  cdlemg11aq  40105  cdlemg10a  40107  cdlemg12g  40116  cdlemg12  40117  cdlemg13  40119  cdlemg17pq  40139  cdlemg18b  40146  cdlemg18c  40147  cdlemg19  40151  cdlemg21  40153  cdlemk7  40315  cdlemk7u  40337  cdlemkfid1N  40388  dia2dimlem1  40531  dia2dimlem3  40533  dihjatcclem3  40887  dihjat  40890

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »