Proof of Theorem dalem2
Step | Hyp | Ref
| Expression |
1 | | dalema.ph |
. . . 4
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
2 | 1 | dalemkehl 36753 |
. . 3
⊢ (𝜑 → 𝐾 ∈ HL) |
3 | 1 | dalempea 36756 |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
4 | 1 | dalemqea 36757 |
. . 3
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
5 | 1 | dalemsea 36759 |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
6 | 1 | dalemtea 36760 |
. . 3
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
7 | | dalemc.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
8 | | dalemc.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
9 | 7, 8 | hlatj4 36504 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑆 ∨ 𝑇)) = ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑇))) |
10 | 2, 3, 4, 5, 6, 9 | syl122anc 1375 |
. 2
⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∨ (𝑆 ∨ 𝑇)) = ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑇))) |
11 | | dalemc.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
12 | | dalem1.o |
. . . . 5
⊢ 𝑂 = (LPlanes‘𝐾) |
13 | | dalem1.y |
. . . . 5
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) |
14 | 1, 11, 7, 8, 12, 13 | dalempjsen 36783 |
. . . 4
⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (LLines‘𝐾)) |
15 | 1, 11, 7, 8, 12, 13 | dalemqnet 36782 |
. . . . 5
⊢ (𝜑 → 𝑄 ≠ 𝑇) |
16 | | eqid 2821 |
. . . . . 6
⊢
(LLines‘𝐾) =
(LLines‘𝐾) |
17 | 7, 8, 16 | llni2 36642 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ 𝑄 ≠ 𝑇) → (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) |
18 | 2, 4, 6, 15, 17 | syl31anc 1369 |
. . . 4
⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) |
19 | 1, 11, 7, 8, 12, 13 | dalem1 36789 |
. . . 4
⊢ (𝜑 → (𝑃 ∨ 𝑆) ≠ (𝑄 ∨ 𝑇)) |
20 | 1, 11, 7, 8, 12, 13 | dalemcea 36790 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
21 | 1 | dalemclpjs 36764 |
. . . . 5
⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆)) |
22 | 1 | dalemclqjt 36765 |
. . . . 5
⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇)) |
23 | | eqid 2821 |
. . . . . 6
⊢
(meet‘𝐾) =
(meet‘𝐾) |
24 | | eqid 2821 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
25 | 11, 23, 24, 8, 16 | 2llnm4 36700 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝐶 ∈ 𝐴 ∧ (𝑃 ∨ 𝑆) ∈ (LLines‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇))) → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ≠ (0.‘𝐾)) |
26 | 2, 20, 14, 18, 21, 22, 25 | syl132anc 1384 |
. . . 4
⊢ (𝜑 → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ≠ (0.‘𝐾)) |
27 | 23, 24, 8, 16 | 2llnmat 36654 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑆) ∈ (LLines‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) ∧ ((𝑃 ∨ 𝑆) ≠ (𝑄 ∨ 𝑇) ∧ ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ≠ (0.‘𝐾))) → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ 𝐴) |
28 | 2, 14, 18, 19, 26, 27 | syl32anc 1374 |
. . 3
⊢ (𝜑 → ((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ 𝐴) |
29 | 7, 23, 8, 16, 12 | 2llnmj 36690 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∨ 𝑆) ∈ (LLines‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (LLines‘𝐾)) → (((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ 𝐴 ↔ ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑇)) ∈ 𝑂)) |
30 | 2, 14, 18, 29 | syl3anc 1367 |
. . 3
⊢ (𝜑 → (((𝑃 ∨ 𝑆)(meet‘𝐾)(𝑄 ∨ 𝑇)) ∈ 𝐴 ↔ ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑇)) ∈ 𝑂)) |
31 | 28, 30 | mpbid 234 |
. 2
⊢ (𝜑 → ((𝑃 ∨ 𝑆) ∨ (𝑄 ∨ 𝑇)) ∈ 𝑂) |
32 | 10, 31 | eqeltrd 2913 |
1
⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∨ (𝑆 ∨ 𝑇)) ∈ 𝑂) |