Proof of Theorem cdleme8
Step | Hyp | Ref
| Expression |
1 | | cdleme8.4 |
. . 3
⊢ 𝐶 = ((𝑃 ∨ 𝑆) ∧ 𝑊) |
2 | 1 | oveq2i 7286 |
. 2
⊢ (𝑃 ∨ 𝐶) = (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) |
3 | | simp1l 1196 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝐾 ∈ HL) |
4 | | simp2l 1198 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝑃 ∈ 𝐴) |
5 | 3 | hllatd 37378 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝐾 ∈ Lat) |
6 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
7 | | cdleme8.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
8 | 6, 7 | atbase 37303 |
. . . . . 6
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
9 | 4, 8 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝑃 ∈ (Base‘𝐾)) |
10 | 6, 7 | atbase 37303 |
. . . . . 6
⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾)) |
11 | 10 | 3ad2ant3 1134 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝑆 ∈ (Base‘𝐾)) |
12 | | cdleme8.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
13 | 6, 12 | latjcl 18157 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) |
14 | 5, 9, 11, 13 | syl3anc 1370 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) |
15 | | simp1r 1197 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝑊 ∈ 𝐻) |
16 | | cdleme8.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
17 | 6, 16 | lhpbase 38012 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
18 | 15, 17 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝑊 ∈ (Base‘𝐾)) |
19 | | cdleme8.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
20 | 6, 19, 12 | latlej1 18166 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑃 ≤ (𝑃 ∨ 𝑆)) |
21 | 5, 9, 11, 20 | syl3anc 1370 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑆)) |
22 | | cdleme8.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
23 | 6, 19, 12, 22, 7 | atmod3i1 37878 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ 𝑆)) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) = ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑊))) |
24 | 3, 4, 14, 18, 21, 23 | syl131anc 1382 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) = ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑊))) |
25 | | eqid 2738 |
. . . . . 6
⊢
(1.‘𝐾) =
(1.‘𝐾) |
26 | 19, 12, 25, 7, 16 | lhpjat2 38035 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ 𝑊) = (1.‘𝐾)) |
27 | 26 | 3adant3 1131 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑊) = (1.‘𝐾)) |
28 | 27 | oveq2d 7291 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → ((𝑃 ∨ 𝑆) ∧ (𝑃 ∨ 𝑊)) = ((𝑃 ∨ 𝑆) ∧ (1.‘𝐾))) |
29 | | hlol 37375 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
30 | 3, 29 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → 𝐾 ∈ OL) |
31 | 6, 22, 25 | olm11 37241 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ (1.‘𝐾)) = (𝑃 ∨ 𝑆)) |
32 | 30, 14, 31 | syl2anc 584 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → ((𝑃 ∨ 𝑆) ∧ (1.‘𝐾)) = (𝑃 ∨ 𝑆)) |
33 | 24, 28, 32 | 3eqtrd 2782 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)) = (𝑃 ∨ 𝑆)) |
34 | 2, 33 | eqtrid 2790 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝐶) = (𝑃 ∨ 𝑆)) |