![]() |
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 29289 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 5556 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) | |
2 | 1 | 3adant1 1127 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
3 | latjcom.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝐾) | |
4 | latjcom.j | . . . . . . 7 ⊢ ∨ = (join‘𝐾) | |
5 | eqid 2798 | . . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
6 | 3, 4, 5 | islat 17649 | . . . . . 6 ⊢ (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵)))) |
7 | simprl 770 | . . . . . 6 ⊢ ((𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))) → dom ∨ = (𝐵 × 𝐵)) | |
8 | 6, 7 | sylbi 220 | . . . . 5 ⊢ (𝐾 ∈ Lat → dom ∨ = (𝐵 × 𝐵)) |
9 | 8 | 3ad2ant1 1130 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → dom ∨ = (𝐵 × 𝐵)) |
10 | 2, 9 | eleqtrrd 2893 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
11 | opelxpi 5556 | . . . . . 6 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) | |
12 | 11 | ancoms 462 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) |
13 | 12 | 3adant1 1127 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) |
14 | 13, 9 | eleqtrrd 2893 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ dom ∨ ) |
15 | 10, 14 | jca 515 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ )) |
16 | latpos 17652 | . . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
17 | 3, 4 | joincom 17632 | . . 3 ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
18 | 16, 17 | syl3anl1 1409 | . 2 ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
19 | 15, 18 | mpdan 686 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 〈cop 4531 × cxp 5517 dom cdm 5519 ‘cfv 6324 (class class class)co 7135 Basecbs 16475 Posetcpo 17542 joincjn 17546 meetcmee 17547 Latclat 17647 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-lub 17576 df-join 17578 df-lat 17648 |
This theorem is referenced by: latleeqj2 17666 latjlej2 17668 latnle 17687 latmlej12 17693 latj12 17698 latj32 17699 latj13 17700 latj31 17701 latj4rot 17704 mod2ile 17708 latdisdlem 17791 olj02 36522 omllaw4 36542 cmt2N 36546 cmtbr3N 36550 cvlexch2 36625 cvlexchb2 36627 cvlatexchb2 36631 cvlatexch2 36633 cvlatexch3 36634 cvlatcvr2 36638 cvlsupr2 36639 cvlsupr7 36644 cvlsupr8 36645 hlatjcom 36664 hlrelat5N 36697 cvrval5 36711 cvrexch 36716 cvratlem 36717 cvrat 36718 2atlt 36735 cvrat3 36738 cvrat4 36739 cvrat42 36740 4noncolr3 36749 1cvrat 36772 3atlem1 36779 4atlem4d 36898 4atlem12 36908 paddcom 37109 paddasslem2 37117 pmapjat2 37150 atmod2i1 37157 atmod2i2 37158 llnmod2i2 37159 atmod4i1 37162 atmod4i2 37163 dalawlem4 37170 dalawlem9 37175 dalawlem12 37178 lhpjat2 37317 lhple 37338 trljat1 37462 trljat2 37463 cdlemc1 37487 cdlemc6 37492 cdlemd1 37494 cdleme5 37536 cdleme9 37549 cdleme10 37550 cdleme19e 37603 trlcolem 38022 trljco2 38037 cdlemk7 38144 cdlemk7u 38166 cdlemkid1 38218 dih1 38582 dihjatc2N 38608 |
Copyright terms: Public domain | W3C validator |