| 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 18370 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 39633 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
| 2 | eqid 2736 | . . 3 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
| 3 | hlatjcom.a | . . 3 ⊢ 𝐴 = (Atoms‘𝐾) | |
| 4 | 2, 3 | atbase 39559 | . 2 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ (Base‘𝐾)) |
| 5 | 2, 3 | atbase 39559 | . 2 ⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ (Base‘𝐾)) |
| 6 | hlatjcom.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
| 7 | 2, 6 | latjcom 18370 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
| 8 | 1, 4, 5, 7 | syl3an 1160 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ‘cfv 6492 (class class class)co 7358 Basecbs 17136 joincjn 18234 Latclat 18354 Atomscatm 39533 HLchlt 39620 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-lub 18267 df-join 18269 df-lat 18355 df-ats 39537 df-atl 39568 df-cvlat 39592 df-hlat 39621 |
| This theorem is referenced by: hlatj12 39641 hlatjrot 39643 hlatlej2 39646 atbtwnex 39718 3noncolr2 39719 hlatcon2 39722 3dimlem2 39729 3dimlem3 39731 3dimlem3OLDN 39732 3dimlem4 39734 3dimlem4OLDN 39735 ps-1 39747 hlatexch4 39751 lplnribN 39821 4atlem10 39876 4atlem11 39879 dalemswapyz 39926 dalem-cly 39941 dalemswapyzps 39960 dalem24 39967 dalem25 39968 dalem44 39986 2llnma1 40057 2llnma3r 40058 2llnma2rN 40060 llnexchb2 40139 dalawlem4 40144 dalawlem5 40145 dalawlem9 40149 dalawlem11 40151 dalawlem12 40152 dalawlem15 40155 4atexlemex2 40341 4atexlemcnd 40342 ltrncnv 40416 trlcnv 40435 cdlemc6 40466 cdleme7aa 40512 cdleme12 40541 cdleme15a 40544 cdleme15c 40546 cdleme17c 40558 cdlemeda 40568 cdleme19a 40573 cdleme19e 40577 cdleme20bN 40580 cdleme20g 40585 cdleme20m 40593 cdleme21c 40597 cdleme22f 40616 cdleme22g 40618 cdleme35b 40720 cdleme35f 40724 cdleme37m 40732 cdleme39a 40735 cdleme42h 40752 cdleme43aN 40759 cdleme43bN 40760 cdleme43dN 40762 cdleme46f2g2 40763 cdleme46f2g1 40764 cdlemeg46c 40783 cdlemeg46nlpq 40787 cdlemeg46ngfr 40788 cdlemeg46rgv 40798 cdlemeg46gfv 40800 cdlemg2kq 40872 cdlemg4a 40878 cdlemg4d 40883 cdlemg4 40887 cdlemg8c 40899 cdlemg11aq 40908 cdlemg10a 40910 cdlemg12g 40919 cdlemg12 40920 cdlemg13 40922 cdlemg17pq 40942 cdlemg18b 40949 cdlemg18c 40950 cdlemg19 40954 cdlemg21 40956 cdlemk7 41118 cdlemk7u 41140 cdlemkfid1N 41191 dia2dimlem1 41334 dia2dimlem3 41336 dihjatcclem3 41690 dihjat 41693 |
| Copyright terms: Public domain | W3C validator |