![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latmcom | Structured version Visualization version GIF version |
Description: The join of a lattice commutes. (Contributed by NM, 6-Nov-2011.) |
Ref | Expression |
---|---|
latmcom.b | ⊢ 𝐵 = (Base‘𝐾) |
latmcom.m | ⊢ ∧ = (meet‘𝐾) |
Ref | Expression |
---|---|
latmcom | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxpi 5670 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) | |
2 | 1 | 3adant1 1130 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
3 | latmcom.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝐾) | |
4 | eqid 2736 | . . . . . . 7 ⊢ (join‘𝐾) = (join‘𝐾) | |
5 | latmcom.m | . . . . . . 7 ⊢ ∧ = (meet‘𝐾) | |
6 | 3, 4, 5 | islat 18322 | . . . . . 6 ⊢ (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom (join‘𝐾) = (𝐵 × 𝐵) ∧ dom ∧ = (𝐵 × 𝐵)))) |
7 | simprr 771 | . . . . . 6 ⊢ ((𝐾 ∈ Poset ∧ (dom (join‘𝐾) = (𝐵 × 𝐵) ∧ dom ∧ = (𝐵 × 𝐵))) → dom ∧ = (𝐵 × 𝐵)) | |
8 | 6, 7 | sylbi 216 | . . . . 5 ⊢ (𝐾 ∈ Lat → dom ∧ = (𝐵 × 𝐵)) |
9 | 8 | 3ad2ant1 1133 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → dom ∧ = (𝐵 × 𝐵)) |
10 | 2, 9 | eleqtrrd 2841 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∧ ) |
11 | opelxpi 5670 | . . . . . 6 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) | |
12 | 11 | ancoms 459 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) |
13 | 12 | 3adant1 1130 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) |
14 | 13, 9 | eleqtrrd 2841 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ dom ∧ ) |
15 | 10, 14 | jca 512 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom ∧ ∧ 〈𝑌, 𝑋〉 ∈ dom ∧ )) |
16 | latpos 18327 | . . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
17 | 3, 5 | meetcom 18293 | . . 3 ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∧ ∧ 〈𝑌, 𝑋〉 ∈ dom ∧ )) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
18 | 16, 17 | syl3anl1 1412 | . 2 ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∧ ∧ 〈𝑌, 𝑋〉 ∈ dom ∧ )) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
19 | 15, 18 | mpdan 685 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 〈cop 4592 × cxp 5631 dom cdm 5633 ‘cfv 6496 (class class class)co 7357 Basecbs 17083 Posetcpo 18196 joincjn 18200 meetcmee 18201 Latclat 18320 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-glb 18236 df-meet 18238 df-lat 18321 |
This theorem is referenced by: latleeqm2 18357 latmlem2 18359 latmlej21 18369 latmlej22 18370 mod2ile 18383 olm12 37690 latm12 37692 latm32 37693 latmrot 37694 olm02 37699 omllaw2N 37706 cmtcomlemN 37710 cmtbr3N 37716 omlfh1N 37720 omlmod1i2N 37722 omlspjN 37723 cvlcvrp 37802 intnatN 37870 cvrexch 37883 cvrat4 37906 2atjm 37908 1cvrat 37939 2at0mat0 37988 dalem4 38128 dalem56 38191 atmod2i1 38324 atmod2i2 38325 llnmod2i2 38326 atmod3i1 38327 atmod3i2 38328 llnexchb2lem 38331 dalawlem3 38336 dalawlem4 38337 dalawlem6 38339 dalawlem9 38342 dalawlem11 38344 dalawlem12 38345 dalawlem15 38348 lhpmcvr 38486 4atexlemc 38532 cdleme20zN 38764 cdleme20d 38775 cdleme20l 38785 cdleme20m 38786 cdlemg12 39113 cdlemg17 39140 cdlemg19 39147 cdlemg44a 39194 dihmeetlem17N 39786 dihmeetlem20N 39789 dihmeetALTN 39790 |
Copyright terms: Public domain | W3C validator |