Proof of Theorem dalem17
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dalema.ph | . . . 4
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) | 
| 2 | 1 | dalemclrju 39638 | . . 3
⊢ (𝜑 → 𝐶 ≤ (𝑅 ∨ 𝑈)) | 
| 3 | 2 | adantr 480 | . 2
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝐶 ≤ (𝑅 ∨ 𝑈)) | 
| 4 | 1 | dalemkelat 39626 | . . . . . 6
⊢ (𝜑 → 𝐾 ∈ Lat) | 
| 5 |  | dalemc.j | . . . . . . 7
⊢  ∨ =
(join‘𝐾) | 
| 6 |  | dalemc.a | . . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) | 
| 7 | 1, 5, 6 | dalempjqeb 39647 | . . . . . 6
⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) | 
| 8 | 1, 6 | dalemreb 39643 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ (Base‘𝐾)) | 
| 9 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 10 |  | dalemc.l | . . . . . . 7
⊢  ≤ =
(le‘𝐾) | 
| 11 | 9, 10, 5 | latlej2 18494 | . . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | 
| 12 | 4, 7, 8, 11 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | 
| 13 |  | dalem17.y | . . . . 5
⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) | 
| 14 | 12, 13 | breqtrrdi 5185 | . . . 4
⊢ (𝜑 → 𝑅 ≤ 𝑌) | 
| 15 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝑅 ≤ 𝑌) | 
| 16 | 1, 5, 6 | dalemsjteb 39648 | . . . . . . 7
⊢ (𝜑 → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) | 
| 17 | 1, 6 | dalemueb 39646 | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾)) | 
| 18 | 9, 10, 5 | latlej2 18494 | . . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → 𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) | 
| 19 | 4, 16, 17, 18 | syl3anc 1373 | . . . . . 6
⊢ (𝜑 → 𝑈 ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) | 
| 20 |  | dalem17.z | . . . . . 6
⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) | 
| 21 | 19, 20 | breqtrrdi 5185 | . . . . 5
⊢ (𝜑 → 𝑈 ≤ 𝑍) | 
| 22 | 21 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝑈 ≤ 𝑍) | 
| 23 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝑌 = 𝑍) | 
| 24 | 22, 23 | breqtrrd 5171 | . . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝑈 ≤ 𝑌) | 
| 25 |  | dalem17.o | . . . . . 6
⊢ 𝑂 = (LPlanes‘𝐾) | 
| 26 | 1, 25 | dalemyeb 39651 | . . . . 5
⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾)) | 
| 27 | 9, 10, 5 | latjle12 18495 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾))) → ((𝑅 ≤ 𝑌 ∧ 𝑈 ≤ 𝑌) ↔ (𝑅 ∨ 𝑈) ≤ 𝑌)) | 
| 28 | 4, 8, 17, 26, 27 | syl13anc 1374 | . . . 4
⊢ (𝜑 → ((𝑅 ≤ 𝑌 ∧ 𝑈 ≤ 𝑌) ↔ (𝑅 ∨ 𝑈) ≤ 𝑌)) | 
| 29 | 28 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → ((𝑅 ≤ 𝑌 ∧ 𝑈 ≤ 𝑌) ↔ (𝑅 ∨ 𝑈) ≤ 𝑌)) | 
| 30 | 15, 24, 29 | mpbi2and 712 | . 2
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → (𝑅 ∨ 𝑈) ≤ 𝑌) | 
| 31 | 1, 6 | dalemceb 39640 | . . . 4
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) | 
| 32 | 1 | dalemkehl 39625 | . . . . 5
⊢ (𝜑 → 𝐾 ∈ HL) | 
| 33 | 1 | dalemrea 39630 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝐴) | 
| 34 | 1 | dalemuea 39633 | . . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐴) | 
| 35 | 9, 5, 6 | hlatjcl 39368 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾)) | 
| 36 | 32, 33, 34, 35 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾)) | 
| 37 | 9, 10 | lattr 18489 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑈) ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾))) → ((𝐶 ≤ (𝑅 ∨ 𝑈) ∧ (𝑅 ∨ 𝑈) ≤ 𝑌) → 𝐶 ≤ 𝑌)) | 
| 38 | 4, 31, 36, 26, 37 | syl13anc 1374 | . . 3
⊢ (𝜑 → ((𝐶 ≤ (𝑅 ∨ 𝑈) ∧ (𝑅 ∨ 𝑈) ≤ 𝑌) → 𝐶 ≤ 𝑌)) | 
| 39 | 38 | adantr 480 | . 2
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → ((𝐶 ≤ (𝑅 ∨ 𝑈) ∧ (𝑅 ∨ 𝑈) ≤ 𝑌) → 𝐶 ≤ 𝑌)) | 
| 40 | 3, 30, 39 | mp2and 699 | 1
⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝐶 ≤ 𝑌) |