![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlatjcom | Structured version Visualization version GIF version |
Description: Commutatitivity of join operation. Frequently-used special case of latjcom 18504 for atoms. (Contributed by NM, 15-Jun-2012.) |
Ref | Expression |
---|---|
hlatjcom.j | ⊢ ∨ = (join‘𝐾) |
hlatjcom.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
hlatjcom | ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hllat 39344 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
2 | eqid 2734 | . . 3 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
3 | hlatjcom.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
4 | 2, 3 | atbase 39270 | . 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ (Base‘𝐾)) |
5 | 2, 3 | atbase 39270 | . 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ (Base‘𝐾)) |
6 | hlatjcom.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
7 | 2, 6 | latjcom 18504 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
8 | 1, 4, 5, 7 | syl3an 1159 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1536 ∈ wcel 2105 ‘cfv 6562 (class class class)co 7430 Basecbs 17244 joincjn 18368 Latclat 18488 Atomscatm 39244 HLchlt 39331 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-lub 18403 df-join 18405 df-lat 18489 df-ats 39248 df-atl 39279 df-cvlat 39303 df-hlat 39332 |
This theorem is referenced by: hlatj12 39352 hlatjrot 39354 hlatlej2 39357 atbtwnex 39430 3noncolr2 39431 hlatcon2 39434 3dimlem2 39441 3dimlem3 39443 3dimlem3OLDN 39444 3dimlem4 39446 3dimlem4OLDN 39447 ps-1 39459 hlatexch4 39463 lplnribN 39533 4atlem10 39588 4atlem11 39591 dalemswapyz 39638 dalem-cly 39653 dalemswapyzps 39672 dalem24 39679 dalem25 39680 dalem44 39698 2llnma1 39769 2llnma3r 39770 2llnma2rN 39772 llnexchb2 39851 dalawlem4 39856 dalawlem5 39857 dalawlem9 39861 dalawlem11 39863 dalawlem12 39864 dalawlem15 39867 4atexlemex2 40053 4atexlemcnd 40054 ltrncnv 40128 trlcnv 40147 cdlemc6 40178 cdleme7aa 40224 cdleme12 40253 cdleme15a 40256 cdleme15c 40258 cdleme17c 40270 cdlemeda 40280 cdleme19a 40285 cdleme19e 40289 cdleme20bN 40292 cdleme20g 40297 cdleme20m 40305 cdleme21c 40309 cdleme22f 40328 cdleme22g 40330 cdleme35b 40432 cdleme35f 40436 cdleme37m 40444 cdleme39a 40447 cdleme42h 40464 cdleme43aN 40471 cdleme43bN 40472 cdleme43dN 40474 cdleme46f2g2 40475 cdleme46f2g1 40476 cdlemeg46c 40495 cdlemeg46nlpq 40499 cdlemeg46ngfr 40500 cdlemeg46rgv 40510 cdlemeg46gfv 40512 cdlemg2kq 40584 cdlemg4a 40590 cdlemg4d 40595 cdlemg4 40599 cdlemg8c 40611 cdlemg11aq 40620 cdlemg10a 40622 cdlemg12g 40631 cdlemg12 40632 cdlemg13 40634 cdlemg17pq 40654 cdlemg18b 40661 cdlemg18c 40662 cdlemg19 40666 cdlemg21 40668 cdlemk7 40830 cdlemk7u 40852 cdlemkfid1N 40903 dia2dimlem1 41046 dia2dimlem3 41048 dihjatcclem3 41402 dihjat 41405 |
Copyright terms: Public domain | W3C validator |