Proof of Theorem dalemcea
Step | Hyp | Ref
| Expression |
1 | | dalema.ph |
. . . 4
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
2 | 1 | dalemkeop 37376 |
. . 3
⊢ (𝜑 → 𝐾 ∈ OP) |
3 | | dalemc.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
4 | 1, 3 | dalemceb 37389 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) |
5 | 1 | dalemkehl 37374 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ HL) |
6 | | dalemc.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
7 | | dalemc.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
8 | | dalem1.o |
. . . . 5
⊢ 𝑂 = (LPlanes‘𝐾) |
9 | | dalem1.y |
. . . . 5
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
10 | 1, 6, 7, 3, 8, 9 | dalempjsen 37404 |
. . . 4
⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (LLines‘𝐾)) |
11 | 1 | dalemqea 37378 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
12 | 1 | dalemtea 37381 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
13 | 1, 6, 7, 3, 8, 9 | dalemqnet 37403 |
. . . . 5
⊢ (𝜑 → 𝑄 ≠ 𝑇) |
14 | | eqid 2737 |
. . . . . 6
⊢
(LLines‘𝐾) =
(LLines‘𝐾) |
15 | 7, 3, 14 | llni2 37263 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ 𝑄 ≠ 𝑇) → (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) |
16 | 5, 11, 12, 13, 15 | syl31anc 1375 |
. . . 4
⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) |
17 | 1, 6, 7, 3, 8, 9 | dalem1 37410 |
. . . 4
⊢ (𝜑 → (𝑃 ∨ 𝑆) ≠ (𝑄 ∨ 𝑇)) |
18 | 1 | dalem-clpjq 37388 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) |
19 | 1, 7, 3 | dalempjqeb 37396 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
20 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝐾) =
(Base‘𝐾) |
21 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0.‘𝐾) =
(0.‘𝐾) |
22 | 20, 6, 21 | op0le 36937 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ OP ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (0.‘𝐾) ≤ (𝑃 ∨ 𝑄)) |
23 | 2, 19, 22 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (0.‘𝐾) ≤ (𝑃 ∨ 𝑄)) |
24 | | breq1 5056 |
. . . . . . . . . 10
⊢ (𝐶 = (0.‘𝐾) → (𝐶 ≤ (𝑃 ∨ 𝑄) ↔ (0.‘𝐾) ≤ (𝑃 ∨ 𝑄))) |
25 | 23, 24 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 = (0.‘𝐾) → 𝐶 ≤ (𝑃 ∨ 𝑄))) |
26 | 25 | necon3bd 2954 |
. . . . . . . 8
⊢ (𝜑 → (¬ 𝐶 ≤ (𝑃 ∨ 𝑄) → 𝐶 ≠ (0.‘𝐾))) |
27 | 18, 26 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ≠ (0.‘𝐾)) |
28 | | eqid 2737 |
. . . . . . . . 9
⊢
(lt‘𝐾) =
(lt‘𝐾) |
29 | 20, 28, 21 | opltn0 36941 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝐶 ∈ (Base‘𝐾)) → ((0.‘𝐾)(lt‘𝐾)𝐶 ↔ 𝐶 ≠ (0.‘𝐾))) |
30 | 2, 4, 29 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((0.‘𝐾)(lt‘𝐾)𝐶 ↔ 𝐶 ≠ (0.‘𝐾))) |
31 | 27, 30 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → (0.‘𝐾)(lt‘𝐾)𝐶) |
32 | 1 | dalemclpjs 37385 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆)) |
33 | 1 | dalemclqjt 37386 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇)) |
34 | 1 | dalemkelat 37375 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Lat) |
35 | 1 | dalempea 37377 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
36 | 1 | dalemsea 37380 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
37 | 20, 7, 3 | hlatjcl 37118 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) |
38 | 5, 35, 36, 37 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) |
39 | 20, 7, 3 | hlatjcl 37118 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) |
40 | 5, 11, 12, 39 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) |
41 | | eqid 2737 |
. . . . . . . . 9
⊢
(meet‘𝐾) =
(meet‘𝐾) |
42 | 20, 6, 41 | latlem12 17972 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))) → ((𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇)) ↔ 𝐶 ≤ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)))) |
43 | 34, 4, 38, 40, 42 | syl13anc 1374 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇)) ↔ 𝐶 ≤ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)))) |
44 | 32, 33, 43 | mpbi2and 712 |
. . . . . 6
⊢ (𝜑 → 𝐶 ≤ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇))) |
45 | | opposet 36932 |
. . . . . . . 8
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset) |
46 | 2, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Poset) |
47 | 20, 21 | op0cl 36935 |
. . . . . . . 8
⊢ (𝐾 ∈ OP →
(0.‘𝐾) ∈
(Base‘𝐾)) |
48 | 2, 47 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0.‘𝐾) ∈ (Base‘𝐾)) |
49 | 20, 41 | latmcl 17946 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ (Base‘𝐾)) |
50 | 34, 38, 40, 49 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ (Base‘𝐾)) |
51 | 20, 6, 28 | pltletr 17849 |
. . . . . . 7
⊢ ((𝐾 ∈ Poset ∧
((0.‘𝐾) ∈
(Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ (Base‘𝐾))) → (((0.‘𝐾)(lt‘𝐾)𝐶 ∧ 𝐶 ≤ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇))) → (0.‘𝐾)(lt‘𝐾)((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)))) |
52 | 46, 48, 4, 50, 51 | syl13anc 1374 |
. . . . . 6
⊢ (𝜑 → (((0.‘𝐾)(lt‘𝐾)𝐶 ∧ 𝐶 ≤ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇))) → (0.‘𝐾)(lt‘𝐾)((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)))) |
53 | 31, 44, 52 | mp2and 699 |
. . . . 5
⊢ (𝜑 → (0.‘𝐾)(lt‘𝐾)((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇))) |
54 | 20, 28, 21 | opltn0 36941 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ (Base‘𝐾)) → ((0.‘𝐾)(lt‘𝐾)((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ↔ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ≠ (0.‘𝐾))) |
55 | 2, 50, 54 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((0.‘𝐾)(lt‘𝐾)((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ↔ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ≠ (0.‘𝐾))) |
56 | 53, 55 | mpbid 235 |
. . . 4
⊢ (𝜑 → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ≠ (0.‘𝐾)) |
57 | 41, 21, 3, 14 | 2llnmat 37275 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑆) ∈ (LLines‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) ∧ ((𝑃 ∨ 𝑆) ≠ (𝑄 ∨ 𝑇) ∧ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ≠ (0.‘𝐾))) → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ 𝐴) |
58 | 5, 10, 16, 17, 56, 57 | syl32anc 1380 |
. . 3
⊢ (𝜑 → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ 𝐴) |
59 | 20, 6, 21, 3 | leat2 37045 |
. . 3
⊢ (((𝐾 ∈ OP ∧ 𝐶 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ 𝐴) ∧ (𝐶 ≠ (0.‘𝐾) ∧ 𝐶 ≤ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)))) → 𝐶 = ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇))) |
60 | 2, 4, 58, 27, 44, 59 | syl32anc 1380 |
. 2
⊢ (𝜑 → 𝐶 = ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇))) |
61 | 60, 58 | eqeltrd 2838 |
1
⊢ (𝜑 → 𝐶 ∈ 𝐴) |