Proof of Theorem cdleme10
Step | Hyp | Ref
| Expression |
1 | | cdleme10.d |
. . 3
⊢ 𝐷 = ((𝑅 ∨ 𝑆) ∧ 𝑊) |
2 | 1 | oveq2i 6661 |
. 2
⊢ (𝑆 ∨ 𝐷) = (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) |
3 | | simp1l 1085 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ HL) |
4 | | simp3l 1089 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑆 ∈ 𝐴) |
5 | | simp2 1062 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑅 ∈ 𝐴) |
6 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
7 | | cdleme10.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
8 | | cdleme10.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
9 | 6, 7, 8 | hlatjcl 34653 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾)) |
10 | 3, 5, 4, 9 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾)) |
11 | | simp1r 1086 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
12 | | cdleme10.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
13 | 6, 12 | lhpbase 35284 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
14 | 11, 13 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾)) |
15 | | hllat 34650 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
16 | 3, 15 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ Lat) |
17 | 6, 8 | atbase 34576 |
. . . . . 6
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾)) |
18 | 17 | 3ad2ant2 1083 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑅 ∈ (Base‘𝐾)) |
19 | 6, 8 | atbase 34576 |
. . . . . 6
⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾)) |
20 | 4, 19 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑆 ∈ (Base‘𝐾)) |
21 | | cdleme10.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
22 | 6, 21, 7 | latlej2 17061 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → 𝑆 ≤ (𝑅 ∨ 𝑆)) |
23 | 16, 18, 20, 22 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝑆 ≤ (𝑅 ∨ 𝑆)) |
24 | | cdleme10.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
25 | 6, 21, 7, 24, 8 | atmod3i1 35150 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑆 ≤ (𝑅 ∨ 𝑆)) → (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) = ((𝑅 ∨ 𝑆) ∧ (𝑆 ∨ 𝑊))) |
26 | 3, 4, 10, 14, 23, 25 | syl131anc 1339 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) = ((𝑅 ∨ 𝑆) ∧ (𝑆 ∨ 𝑊))) |
27 | 6, 7 | latjcom 17059 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝑅 ∨ 𝑆) = (𝑆 ∨ 𝑅)) |
28 | 16, 18, 20, 27 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑅 ∨ 𝑆) = (𝑆 ∨ 𝑅)) |
29 | | eqid 2622 |
. . . . . 6
⊢
(1.‘𝐾) =
(1.‘𝐾) |
30 | 21, 7, 29, 8, 12 | lhpjat2 35307 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝑊) = (1.‘𝐾)) |
31 | 30 | 3adant2 1080 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝑊) = (1.‘𝐾)) |
32 | 28, 31 | oveq12d 6668 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝑅 ∨ 𝑆) ∧ (𝑆 ∨ 𝑊)) = ((𝑆 ∨ 𝑅) ∧ (1.‘𝐾))) |
33 | | hlol 34648 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
34 | 3, 33 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → 𝐾 ∈ OL) |
35 | 6, 7 | latjcl 17051 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑆 ∨ 𝑅) ∈ (Base‘𝐾)) |
36 | 16, 20, 18, 35 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝑅) ∈ (Base‘𝐾)) |
37 | 6, 24, 29 | olm11 34514 |
. . . 4
⊢ ((𝐾 ∈ OL ∧ (𝑆 ∨ 𝑅) ∈ (Base‘𝐾)) → ((𝑆 ∨ 𝑅) ∧ (1.‘𝐾)) = (𝑆 ∨ 𝑅)) |
38 | 34, 36, 37 | syl2anc 693 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → ((𝑆 ∨ 𝑅) ∧ (1.‘𝐾)) = (𝑆 ∨ 𝑅)) |
39 | 26, 32, 38 | 3eqtrd 2660 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)) = (𝑆 ∨ 𝑅)) |
40 | 2, 39 | syl5eq 2668 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴 ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) → (𝑆 ∨ 𝐷) = (𝑆 ∨ 𝑅)) |