Proof of Theorem cdleme10
| Step | Hyp | Ref
| Expression |
| 1 | | cdleme10.d |
. . 3
⊢ 𝐷 = ((𝑅 ∨ 𝑆) ∧ 𝑊) |
| 2 | 1 | oveq2i 7442 |
. 2
⊢ (𝑆 ∨ 𝐷) = (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) |
| 3 | | simp1l 1198 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ HL) |
| 4 | | simp3l 1202 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑆 ∈ 𝐴) |
| 5 | | simp2 1138 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑅 ∈ 𝐴) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 7 | | cdleme10.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
| 8 | | cdleme10.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
| 9 | 6, 7, 8 | hlatjcl 39368 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾)) |
| 10 | 3, 5, 4, 9 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾)) |
| 11 | | simp1r 1199 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
| 12 | | cdleme10.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
| 13 | 6, 12 | lhpbase 40000 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
| 14 | 11, 13 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾)) |
| 15 | 3 | hllatd 39365 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ Lat) |
| 16 | 6, 8 | atbase 39290 |
. . . . . 6
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾)) |
| 17 | 16 | 3ad2ant2 1135 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑅 ∈ (Base‘𝐾)) |
| 18 | 6, 8 | atbase 39290 |
. . . . . 6
⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾)) |
| 19 | 4, 18 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑆 ∈ (Base‘𝐾)) |
| 20 | | cdleme10.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 21 | 6, 20, 7 | latlej2 18494 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 ≤ (𝑅 ∨ 𝑆)) |
| 22 | 15, 17, 19, 21 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑆 ≤ (𝑅 ∨ 𝑆)) |
| 23 | | cdleme10.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
| 24 | 6, 20, 7, 23, 8 | atmod3i1 39866 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑆 ≤ (𝑅 ∨ 𝑆)) → (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) = ((𝑅 ∨ 𝑆) ∧ (𝑆 ∨ 𝑊))) |
| 25 | 3, 4, 10, 14, 22, 24 | syl131anc 1385 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) = ((𝑅 ∨ 𝑆) ∧ (𝑆 ∨ 𝑊))) |
| 26 | 6, 7 | latjcom 18492 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑅 ∨ 𝑆) = (𝑆 ∨ 𝑅)) |
| 27 | 15, 17, 19, 26 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ 𝑆) = (𝑆 ∨ 𝑅)) |
| 28 | | eqid 2737 |
. . . . . 6
⊢
(1.‘𝐾) =
(1.‘𝐾) |
| 29 | 20, 7, 28, 8, 12 | lhpjat2 40023 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝑊) = (1.‘𝐾)) |
| 30 | 29 | 3adant2 1132 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝑊) = (1.‘𝐾)) |
| 31 | 27, 30 | oveq12d 7449 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝑅 ∨ 𝑆) ∧ (𝑆 ∨ 𝑊)) = ((𝑆 ∨ 𝑅) ∧ (1.‘𝐾))) |
| 32 | | hlol 39362 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
| 33 | 3, 32 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ OL) |
| 34 | 6, 7 | latjcl 18484 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑆 ∨ 𝑅) ∈ (Base‘𝐾)) |
| 35 | 15, 19, 17, 34 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝑅) ∈ (Base‘𝐾)) |
| 36 | 6, 23, 28 | olm11 39228 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ (𝑆 ∨ 𝑅) ∈ (Base‘𝐾)) → ((𝑆 ∨ 𝑅) ∧ (1.‘𝐾)) = (𝑆 ∨ 𝑅)) |
| 37 | 33, 35, 36 | syl2anc 584 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝑆 ∨ 𝑅) ∧ (1.‘𝐾)) = (𝑆 ∨ 𝑅)) |
| 38 | 25, 31, 37 | 3eqtrd 2781 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) = (𝑆 ∨ 𝑅)) |
| 39 | 2, 38 | eqtrid 2789 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝐷) = (𝑆 ∨ 𝑅)) |