![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2llnm4 | Structured version Visualization version GIF version |
Description: Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012.) |
Ref | Expression |
---|---|
2llnm4.l | ⊢ ≤ = (le‘𝐾) |
2llnm4.m | ⊢ ∧ = (meet‘𝐾) |
2llnm4.z | ⊢ 0 = (0.‘𝐾) |
2llnm4.a | ⊢ 𝐴 = (Atoms‘𝐾) |
2llnm4.n | ⊢ 𝑁 = (LLines‘𝐾) |
Ref | Expression |
---|---|
2llnm4 | ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → (𝑋 ∧ 𝑌) ≠ 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlatl 35889 | . . 3 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) | |
2 | 1 | 3ad2ant1 1113 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝐾 ∈ AtLat) |
3 | hllat 35892 | . . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
4 | 3 | 3ad2ant1 1113 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝐾 ∈ Lat) |
5 | simp22 1187 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝑋 ∈ 𝑁) | |
6 | eqid 2772 | . . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
7 | 2llnm4.n | . . . . 5 ⊢ 𝑁 = (LLines‘𝐾) | |
8 | 6, 7 | llnbase 36038 | . . . 4 ⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ (Base‘𝐾)) |
9 | 5, 8 | syl 17 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝑋 ∈ (Base‘𝐾)) |
10 | simp23 1188 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝑌 ∈ 𝑁) | |
11 | 6, 7 | llnbase 36038 | . . . 4 ⊢ (𝑌 ∈ 𝑁 → 𝑌 ∈ (Base‘𝐾)) |
12 | 10, 11 | syl 17 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝑌 ∈ (Base‘𝐾)) |
13 | 2llnm4.m | . . . 4 ⊢ ∧ = (meet‘𝐾) | |
14 | 6, 13 | latmcl 17510 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾)) |
15 | 4, 9, 12, 14 | syl3anc 1351 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → (𝑋 ∧ 𝑌) ∈ (Base‘𝐾)) |
16 | simp21 1186 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝑃 ∈ 𝐴) | |
17 | simp3 1118 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) | |
18 | 2llnm4.a | . . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾) | |
19 | 6, 18 | atbase 35818 | . . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
20 | 16, 19 | syl 17 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝑃 ∈ (Base‘𝐾)) |
21 | 2llnm4.l | . . . . 5 ⊢ ≤ = (le‘𝐾) | |
22 | 6, 21, 13 | latlem12 17536 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾))) → ((𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌) ↔ 𝑃 ≤ (𝑋 ∧ 𝑌))) |
23 | 4, 20, 9, 12, 22 | syl13anc 1352 | . . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → ((𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌) ↔ 𝑃 ≤ (𝑋 ∧ 𝑌))) |
24 | 17, 23 | mpbid 224 | . 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → 𝑃 ≤ (𝑋 ∧ 𝑌)) |
25 | 2llnm4.z | . . 3 ⊢ 0 = (0.‘𝐾) | |
26 | 6, 21, 25, 18 | atlen0 35839 | . 2 ⊢ (((𝐾 ∈ AtLat ∧ (𝑋 ∧ 𝑌) ∈ (Base‘𝐾) ∧ 𝑃 ∈ 𝐴) ∧ 𝑃 ≤ (𝑋 ∧ 𝑌)) → (𝑋 ∧ 𝑌) ≠ 0 ) |
27 | 2, 15, 16, 24, 26 | syl31anc 1353 | 1 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → (𝑋 ∧ 𝑌) ≠ 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2048 ≠ wne 2961 class class class wbr 4923 ‘cfv 6182 (class class class)co 6970 Basecbs 16329 lecple 16418 meetcmee 17403 0.cp0 17495 Latclat 17503 Atomscatm 35792 AtLatcal 35793 HLchlt 35879 LLinesclln 36020 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5305 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-proset 17386 df-poset 17404 df-plt 17416 df-lub 17432 df-glb 17433 df-join 17434 df-meet 17435 df-p0 17497 df-lat 17504 df-covers 35795 df-ats 35796 df-atl 35827 df-cvlat 35851 df-hlat 35880 df-llines 36027 |
This theorem is referenced by: 2llnmeqat 36100 dalem2 36190 |
Copyright terms: Public domain | W3C validator |