Proof of Theorem cdleme1b
| Step | Hyp | Ref
| Expression |
| 1 | | cdleme1.f |
. 2
⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) |
| 2 | | hllat 39364 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
| 3 | 2 | ad2antrr 726 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐾 ∈ Lat) |
| 4 | | simpr3 1197 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑅 ∈ 𝐴) |
| 5 | | cdleme1.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
| 6 | | cdleme1.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
| 7 | 5, 6 | atbase 39290 |
. . . . 5
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵) |
| 8 | 4, 7 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑅 ∈ 𝐵) |
| 9 | | cdleme1.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 10 | | cdleme1.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
| 11 | | cdleme1.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
| 12 | | cdleme1.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
| 13 | | cdleme1.u |
. . . . . 6
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
| 14 | 9, 10, 11, 6, 12, 13, 5 | cdleme0aa 40212 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑈 ∈ 𝐵) |
| 15 | 14 | 3adant3r3 1185 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑈 ∈ 𝐵) |
| 16 | 5, 10 | latjcl 18484 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ 𝐵 ∧ 𝑈 ∈ 𝐵) → (𝑅 ∨ 𝑈) ∈ 𝐵) |
| 17 | 3, 8, 15, 16 | syl3anc 1373 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑅 ∨ 𝑈) ∈ 𝐵) |
| 18 | | simpr2 1196 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑄 ∈ 𝐴) |
| 19 | 5, 6 | atbase 39290 |
. . . . 5
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵) |
| 20 | 18, 19 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑄 ∈ 𝐵) |
| 21 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑃 ∈ 𝐴) |
| 22 | 5, 6 | atbase 39290 |
. . . . . . 7
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
| 23 | 21, 22 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑃 ∈ 𝐵) |
| 24 | 5, 10 | latjcl 18484 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵) → (𝑃 ∨ 𝑅) ∈ 𝐵) |
| 25 | 3, 23, 8, 24 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑃 ∨ 𝑅) ∈ 𝐵) |
| 26 | 5, 12 | lhpbase 40000 |
. . . . . 6
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
| 27 | 26 | ad2antlr 727 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑊 ∈ 𝐵) |
| 28 | 5, 11 | latmcl 18485 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ∈ 𝐵) |
| 29 | 3, 25, 27, 28 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑅) ∧ 𝑊) ∈ 𝐵) |
| 30 | 5, 10 | latjcl 18484 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ ((𝑃 ∨ 𝑅) ∧ 𝑊) ∈ 𝐵) → (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ∈ 𝐵) |
| 31 | 3, 20, 29, 30 | syl3anc 1373 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ∈ 𝐵) |
| 32 | 5, 11 | latmcl 18485 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑈) ∈ 𝐵 ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)) ∈ 𝐵) → ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ∈ 𝐵) |
| 33 | 3, 17, 31, 32 | syl3anc 1373 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) ∈ 𝐵) |
| 34 | 1, 33 | eqeltrid 2845 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐹 ∈ 𝐵) |