Proof of Theorem cdleme35b
| Step | Hyp | Ref
| Expression |
| 1 | | simp11l 1285 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝐾 ∈ HL) |
| 2 | 1 | hllatd 39365 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝐾 ∈ Lat) |
| 3 | | simp13l 1289 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑄 ∈ 𝐴) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 5 | | cdleme35.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
| 6 | 4, 5 | atbase 39290 |
. . . 4
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
| 7 | 3, 6 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑄 ∈ (Base‘𝐾)) |
| 8 | | simp2rl 1243 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ∈ 𝐴) |
| 9 | | simp11 1204 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 10 | | simp12 1205 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
| 11 | | simp2l 1200 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑄) |
| 12 | | cdleme35.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 13 | | cdleme35.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
| 14 | | cdleme35.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
| 15 | | cdleme35.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
| 16 | | cdleme35.u |
. . . . . 6
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
| 17 | 12, 13, 14, 5, 15, 16 | cdleme0a 40213 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑈 ∈ 𝐴) |
| 18 | 9, 10, 3, 11, 17 | syl112anc 1376 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑈 ∈ 𝐴) |
| 19 | 4, 13, 5 | hlatjcl 39368 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾)) |
| 20 | 1, 8, 18, 19 | syl3anc 1373 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑅 ∨ 𝑈) ∈ (Base‘𝐾)) |
| 21 | 4, 12, 13 | latlej1 18493 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑈) ∈ (Base‘𝐾)) → 𝑄 ≤ (𝑄 ∨ (𝑅 ∨ 𝑈))) |
| 22 | 2, 7, 20, 21 | syl3anc 1373 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑄 ≤ (𝑄 ∨ (𝑅 ∨ 𝑈))) |
| 23 | | simp12l 1287 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ∈ 𝐴) |
| 24 | 4, 5 | atbase 39290 |
. . . . . . 7
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
| 25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ∈ (Base‘𝐾)) |
| 26 | 4, 5 | atbase 39290 |
. . . . . . 7
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾)) |
| 27 | 8, 26 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ∈ (Base‘𝐾)) |
| 28 | 4, 13 | latjcl 18484 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾)) |
| 29 | 2, 25, 27, 28 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾)) |
| 30 | | simp11r 1286 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑊 ∈ 𝐻) |
| 31 | 4, 15 | lhpbase 40000 |
. . . . . 6
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
| 32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑊 ∈ (Base‘𝐾)) |
| 33 | 4, 14 | latmcl 18485 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ∈ (Base‘𝐾)) |
| 34 | 2, 29, 32, 33 | syl3anc 1373 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ∈ (Base‘𝐾)) |
| 35 | 4, 13 | latjcl 18484 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑅) ∨ 𝑄) ∈ (Base‘𝐾)) |
| 36 | 2, 29, 7, 35 | syl3anc 1373 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∨ 𝑄) ∈ (Base‘𝐾)) |
| 37 | 4, 12, 14 | latmle1 18509 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ≤ (𝑃 ∨ 𝑅)) |
| 38 | 2, 29, 32, 37 | syl3anc 1373 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ≤ (𝑃 ∨ 𝑅)) |
| 39 | 4, 12, 13 | latlej1 18493 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑅) ≤ ((𝑃 ∨ 𝑅) ∨ 𝑄)) |
| 40 | 2, 29, 7, 39 | syl3anc 1373 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∨ 𝑅) ≤ ((𝑃 ∨ 𝑅) ∨ 𝑄)) |
| 41 | 4, 12, 2, 34, 29, 36, 38, 40 | lattrd 18491 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ≤ ((𝑃 ∨ 𝑅) ∨ 𝑄)) |
| 42 | 16 | oveq2i 7442 |
. . . . . 6
⊢ (𝑄 ∨ 𝑈) = (𝑄 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) |
| 43 | 4, 13, 5 | hlatjcl 39368 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
| 44 | 1, 23, 3, 43 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
| 45 | 12, 13, 5 | hlatlej2 39377 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄)) |
| 46 | 1, 23, 3, 45 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑄 ≤ (𝑃 ∨ 𝑄)) |
| 47 | 4, 12, 13, 14, 5 | atmod3i1 39866 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑄 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) = ((𝑃 ∨ 𝑄) ∧ (𝑄 ∨ 𝑊))) |
| 48 | 1, 3, 44, 32, 46, 47 | syl131anc 1385 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) = ((𝑃 ∨ 𝑄) ∧ (𝑄 ∨ 𝑊))) |
| 49 | | simp13 1206 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
| 50 | | eqid 2737 |
. . . . . . . . . 10
⊢
(1.‘𝐾) =
(1.‘𝐾) |
| 51 | 12, 13, 50, 5, 15 | lhpjat2 40023 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑄 ∨ 𝑊) = (1.‘𝐾)) |
| 52 | 9, 49, 51 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ 𝑊) = (1.‘𝐾)) |
| 53 | 52 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑄) ∧ (𝑄 ∨ 𝑊)) = ((𝑃 ∨ 𝑄) ∧ (1.‘𝐾))) |
| 54 | | hlol 39362 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
| 55 | 1, 54 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝐾 ∈ OL) |
| 56 | 4, 14, 50 | olm11 39228 |
. . . . . . . 8
⊢ ((𝐾 ∈ OL ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ (1.‘𝐾)) = (𝑃 ∨ 𝑄)) |
| 57 | 55, 44, 56 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑄) ∧ (1.‘𝐾)) = (𝑃 ∨ 𝑄)) |
| 58 | 48, 53, 57 | 3eqtrd 2781 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) = (𝑃 ∨ 𝑄)) |
| 59 | 42, 58 | eqtrid 2789 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ 𝑈) = (𝑃 ∨ 𝑄)) |
| 60 | 59 | oveq2d 7447 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑅 ∨ (𝑄 ∨ 𝑈)) = (𝑅 ∨ (𝑃 ∨ 𝑄))) |
| 61 | 13, 5 | hlatj12 39372 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (𝑄 ∨ (𝑅 ∨ 𝑈)) = (𝑅 ∨ (𝑄 ∨ 𝑈))) |
| 62 | 1, 3, 8, 18, 61 | syl13anc 1374 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ (𝑅 ∨ 𝑈)) = (𝑅 ∨ (𝑄 ∨ 𝑈))) |
| 63 | 13, 5 | hlatjcom 39369 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃)) |
| 64 | 1, 23, 8, 63 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃)) |
| 65 | 64 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∨ 𝑄) = ((𝑅 ∨ 𝑃) ∨ 𝑄)) |
| 66 | 13, 5 | hlatjass 39371 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∨ 𝑄) = (𝑅 ∨ (𝑃 ∨ 𝑄))) |
| 67 | 1, 8, 23, 3, 66 | syl13anc 1374 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ∨ 𝑃) ∨ 𝑄) = (𝑅 ∨ (𝑃 ∨ 𝑄))) |
| 68 | 65, 67 | eqtrd 2777 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∨ 𝑄) = (𝑅 ∨ (𝑃 ∨ 𝑄))) |
| 69 | 60, 62, 68 | 3eqtr4rd 2788 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∨ 𝑄) = (𝑄 ∨ (𝑅 ∨ 𝑈))) |
| 70 | 41, 69 | breqtrd 5169 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ≤ (𝑄 ∨ (𝑅 ∨ 𝑈))) |
| 71 | 4, 13 | latjcl 18484 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑈) ∈ (Base‘𝐾)) → (𝑄 ∨ (𝑅 ∨ 𝑈)) ∈ (Base‘𝐾)) |
| 72 | 2, 7, 20, 71 | syl3anc 1373 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ (𝑅 ∨ 𝑈)) ∈ (Base‘𝐾)) |
| 73 | 4, 12, 13 | latjle12 18495 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑅) ∧ 𝑊) ∈ (Base‘𝐾) ∧ (𝑄 ∨ (𝑅 ∨ 𝑈)) ∈ (Base‘𝐾))) → ((𝑄 ≤ (𝑄 ∨ (𝑅 ∨ 𝑈)) ∧ ((𝑃 ∨ 𝑅) ∧ 𝑊) ≤ (𝑄 ∨ (𝑅 ∨ 𝑈))) ↔ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑅 ∨ 𝑈)))) |
| 74 | 2, 7, 34, 72, 73 | syl13anc 1374 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑄 ≤ (𝑄 ∨ (𝑅 ∨ 𝑈)) ∧ ((𝑃 ∨ 𝑅) ∧ 𝑊) ≤ (𝑄 ∨ (𝑅 ∨ 𝑈))) ↔ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑅 ∨ 𝑈)))) |
| 75 | 22, 70, 74 | mpbi2and 712 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ≤ (𝑄 ∨ (𝑅 ∨ 𝑈))) |