Proof of Theorem cdleme22d
Step | Hyp | Ref
| Expression |
1 | | simp3r 1090 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑆 ≤ (𝑇 ∨ 𝑉)) |
2 | | simp1l 1085 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝐾 ∈ HL) |
3 | | simp22l 1180 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑇 ∈ 𝐴) |
4 | | simp23l 1182 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑉 ∈ 𝐴) |
5 | | cdleme22.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
6 | | cdleme22.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
7 | | cdleme22.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
8 | 5, 6, 7 | hlatlej1 34661 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → 𝑇 ≤ (𝑇 ∨ 𝑉)) |
9 | 2, 3, 4, 8 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑇 ≤ (𝑇 ∨ 𝑉)) |
10 | | hllat 34650 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
11 | 2, 10 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝐾 ∈ Lat) |
12 | | simp21l 1178 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑆 ∈ 𝐴) |
13 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝐾) =
(Base‘𝐾) |
14 | 13, 7 | atbase 34576 |
. . . . . . . 8
⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑆 ∈ (Base‘𝐾)) |
16 | 13, 7 | atbase 34576 |
. . . . . . . 8
⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾)) |
17 | 3, 16 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑇 ∈ (Base‘𝐾)) |
18 | 13, 6, 7 | hlatjcl 34653 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (𝑇 ∨ 𝑉) ∈ (Base‘𝐾)) |
19 | 2, 3, 4, 18 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → (𝑇 ∨ 𝑉) ∈ (Base‘𝐾)) |
20 | 13, 5, 6 | latjle12 17062 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑉) ∈ (Base‘𝐾))) → ((𝑆 ≤ (𝑇 ∨ 𝑉) ∧ 𝑇 ≤ (𝑇 ∨ 𝑉)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑇 ∨ 𝑉))) |
21 | 11, 15, 17, 19, 20 | syl13anc 1328 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑆 ≤ (𝑇 ∨ 𝑉) ∧ 𝑇 ≤ (𝑇 ∨ 𝑉)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑇 ∨ 𝑉))) |
22 | 1, 9, 21 | mpbi2and 956 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → (𝑆 ∨ 𝑇) ≤ (𝑇 ∨ 𝑉)) |
23 | 13, 6, 7 | hlatjcl 34653 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
24 | 2, 12, 3, 23 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
25 | | simp1r 1086 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑊 ∈ 𝐻) |
26 | | cdleme22.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
27 | 13, 26 | lhpbase 35284 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
28 | 25, 27 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑊 ∈ (Base‘𝐾)) |
29 | | cdleme22.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
30 | 13, 5, 29 | latmlem1 17081 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ ((𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑇 ∨ 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑆 ∨ 𝑇) ≤ (𝑇 ∨ 𝑉) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ≤ ((𝑇 ∨ 𝑉) ∧ 𝑊))) |
31 | 11, 24, 19, 28, 30 | syl13anc 1328 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑆 ∨ 𝑇) ≤ (𝑇 ∨ 𝑉) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ≤ ((𝑇 ∨ 𝑉) ∧ 𝑊))) |
32 | 22, 31 | mpd 15 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ≤ ((𝑇 ∨ 𝑉) ∧ 𝑊)) |
33 | | simp1 1061 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
34 | | simp22 1095 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) |
35 | | eqid 2622 |
. . . . . . . 8
⊢
(0.‘𝐾) =
(0.‘𝐾) |
36 | 5, 29, 35, 7, 26 | lhpmat 35316 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) → (𝑇 ∧ 𝑊) = (0.‘𝐾)) |
37 | 33, 34, 36 | syl2anc 693 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → (𝑇 ∧ 𝑊) = (0.‘𝐾)) |
38 | 37 | oveq1d 6665 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑇 ∧ 𝑊) ∨ 𝑉) = ((0.‘𝐾) ∨ 𝑉)) |
39 | | simp23r 1183 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑉 ≤ 𝑊) |
40 | 13, 5, 6, 29, 7 | atmod4i1 35152 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑉 ∈ 𝐴 ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 ≤ 𝑊) → ((𝑇 ∧ 𝑊) ∨ 𝑉) = ((𝑇 ∨ 𝑉) ∧ 𝑊)) |
41 | 2, 4, 17, 28, 39, 40 | syl131anc 1339 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑇 ∧ 𝑊) ∨ 𝑉) = ((𝑇 ∨ 𝑉) ∧ 𝑊)) |
42 | | hlol 34648 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
43 | 2, 42 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝐾 ∈ OL) |
44 | 13, 7 | atbase 34576 |
. . . . . . 7
⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾)) |
45 | 4, 44 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑉 ∈ (Base‘𝐾)) |
46 | 13, 6, 35 | olj02 34513 |
. . . . . 6
⊢ ((𝐾 ∈ OL ∧ 𝑉 ∈ (Base‘𝐾)) → ((0.‘𝐾) ∨ 𝑉) = 𝑉) |
47 | 43, 45, 46 | syl2anc 693 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((0.‘𝐾) ∨ 𝑉) = 𝑉) |
48 | 38, 41, 47 | 3eqtr3d 2664 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑇 ∨ 𝑉) ∧ 𝑊) = 𝑉) |
49 | 32, 48 | breqtrd 4679 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ≤ 𝑉) |
50 | | hlatl 34647 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
51 | 2, 50 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝐾 ∈ AtLat) |
52 | | simp21r 1179 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ¬ 𝑆 ≤ 𝑊) |
53 | | simp3l 1089 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑆 ≠ 𝑇) |
54 | 5, 6, 29, 7, 26 | lhpat 35329 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴) |
55 | 2, 25, 12, 52, 3, 53, 54 | syl222anc 1342 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴) |
56 | 5, 7 | atcmp 34598 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ ((𝑆 ∨ 𝑇) ∧ 𝑊) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (((𝑆 ∨ 𝑇) ∧ 𝑊) ≤ 𝑉 ↔ ((𝑆 ∨ 𝑇) ∧ 𝑊) = 𝑉)) |
57 | 51, 55, 4, 56 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → (((𝑆 ∨ 𝑇) ∧ 𝑊) ≤ 𝑉 ↔ ((𝑆 ∨ 𝑇) ∧ 𝑊) = 𝑉)) |
58 | 49, 57 | mpbid 222 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → ((𝑆 ∨ 𝑇) ∧ 𝑊) = 𝑉) |
59 | 58 | eqcomd 2628 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ (𝑆 ≠ 𝑇 ∧ 𝑆 ≤ (𝑇 ∨ 𝑉))) → 𝑉 = ((𝑆 ∨ 𝑇) ∧ 𝑊)) |