![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latjcom | Structured version Visualization version GIF version |
Description: The join of a lattice commutes. (chjcom 31026 analog.) (Contributed by NM, 16-Sep-2011.) |
Ref | Expression |
---|---|
latjcom.b | β’ π΅ = (BaseβπΎ) |
latjcom.j | β’ β¨ = (joinβπΎ) |
Ref | Expression |
---|---|
latjcom | β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxpi 5712 | . . . . 5 β’ ((π β π΅ β§ π β π΅) β β¨π, πβ© β (π΅ Γ π΅)) | |
2 | 1 | 3adant1 1128 | . . . 4 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β β¨π, πβ© β (π΅ Γ π΅)) |
3 | latjcom.b | . . . . . . 7 β’ π΅ = (BaseβπΎ) | |
4 | latjcom.j | . . . . . . 7 β’ β¨ = (joinβπΎ) | |
5 | eqid 2730 | . . . . . . 7 β’ (meetβπΎ) = (meetβπΎ) | |
6 | 3, 4, 5 | islat 18390 | . . . . . 6 β’ (πΎ β Lat β (πΎ β Poset β§ (dom β¨ = (π΅ Γ π΅) β§ dom (meetβπΎ) = (π΅ Γ π΅)))) |
7 | simprl 767 | . . . . . 6 β’ ((πΎ β Poset β§ (dom β¨ = (π΅ Γ π΅) β§ dom (meetβπΎ) = (π΅ Γ π΅))) β dom β¨ = (π΅ Γ π΅)) | |
8 | 6, 7 | sylbi 216 | . . . . 5 β’ (πΎ β Lat β dom β¨ = (π΅ Γ π΅)) |
9 | 8 | 3ad2ant1 1131 | . . . 4 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β dom β¨ = (π΅ Γ π΅)) |
10 | 2, 9 | eleqtrrd 2834 | . . 3 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β β¨π, πβ© β dom β¨ ) |
11 | opelxpi 5712 | . . . . . 6 β’ ((π β π΅ β§ π β π΅) β β¨π, πβ© β (π΅ Γ π΅)) | |
12 | 11 | ancoms 457 | . . . . 5 β’ ((π β π΅ β§ π β π΅) β β¨π, πβ© β (π΅ Γ π΅)) |
13 | 12 | 3adant1 1128 | . . . 4 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β β¨π, πβ© β (π΅ Γ π΅)) |
14 | 13, 9 | eleqtrrd 2834 | . . 3 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β β¨π, πβ© β dom β¨ ) |
15 | 10, 14 | jca 510 | . 2 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (β¨π, πβ© β dom β¨ β§ β¨π, πβ© β dom β¨ )) |
16 | latpos 18395 | . . 3 β’ (πΎ β Lat β πΎ β Poset) | |
17 | 3, 4 | joincom 18359 | . . 3 β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ (β¨π, πβ© β dom β¨ β§ β¨π, πβ© β dom β¨ )) β (π β¨ π) = (π β¨ π)) |
18 | 16, 17 | syl3anl1 1410 | . 2 β’ (((πΎ β Lat β§ π β π΅ β§ π β π΅) β§ (β¨π, πβ© β dom β¨ β§ β¨π, πβ© β dom β¨ )) β (π β¨ π) = (π β¨ π)) |
19 | 15, 18 | mpdan 683 | 1 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 394 β§ w3a 1085 = wceq 1539 β wcel 2104 β¨cop 4633 Γ cxp 5673 dom cdm 5675 βcfv 6542 (class class class)co 7411 Basecbs 17148 Posetcpo 18264 joincjn 18268 meetcmee 18269 Latclat 18388 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 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 7367 df-ov 7414 df-oprab 7415 df-lub 18303 df-join 18305 df-lat 18389 |
This theorem is referenced by: latleeqj2 18409 latjlej2 18411 latnle 18430 latmlej12 18436 latj12 18441 latj32 18442 latj13 18443 latj31 18444 latj4rot 18447 mod2ile 18451 latdisdlem 18453 olj02 38399 omllaw4 38419 cmt2N 38423 cmtbr3N 38427 cvlexch2 38502 cvlexchb2 38504 cvlatexchb2 38508 cvlatexch2 38510 cvlatexch3 38511 cvlatcvr2 38515 cvlsupr2 38516 cvlsupr7 38521 cvlsupr8 38522 hlatjcom 38541 hlrelat5N 38575 cvrval5 38589 cvrexch 38594 cvratlem 38595 cvrat 38596 2atlt 38613 cvrat3 38616 cvrat4 38617 cvrat42 38618 4noncolr3 38627 1cvrat 38650 3atlem1 38657 4atlem4d 38776 4atlem12 38786 paddcom 38987 paddasslem2 38995 pmapjat2 39028 atmod2i1 39035 atmod2i2 39036 llnmod2i2 39037 atmod4i1 39040 atmod4i2 39041 dalawlem4 39048 dalawlem9 39053 dalawlem12 39056 lhpjat2 39195 lhple 39216 trljat1 39340 trljat2 39341 cdlemc1 39365 cdlemc6 39370 cdlemd1 39372 cdleme5 39414 cdleme9 39427 cdleme10 39428 cdleme19e 39481 trlcolem 39900 trljco2 39915 cdlemk7 40022 cdlemk7u 40044 cdlemkid1 40096 dih1 40460 dihjatc2N 40486 |
Copyright terms: Public domain | W3C validator |