Proof of Theorem cdlemc4
Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → 𝐾 ∈ HL) |
2 | | hllat 33668 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → 𝐾 ∈ Lat) |
4 | | simpl 472 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
5 | | simpr1 1060 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → 𝐹 ∈ 𝑇) |
6 | | simpr2l 1113 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → 𝑃 ∈ 𝐴) |
7 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘𝐾) =
(Base‘𝐾) |
8 | | cdlemc3.a |
. . . . . . . . 9
⊢ 𝐴 = (Atoms‘𝐾) |
9 | 7, 8 | atbase 33594 |
. . . . . . . 8
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
10 | 6, 9 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → 𝑃 ∈ (Base‘𝐾)) |
11 | | cdlemc3.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
12 | | cdlemc3.t |
. . . . . . . 8
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
13 | 7, 11, 12 | ltrncl 34429 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐹‘𝑃) ∈ (Base‘𝐾)) |
14 | 4, 5, 10, 13 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝐹‘𝑃) ∈ (Base‘𝐾)) |
15 | | simpr3l 1115 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → 𝑄 ∈ 𝐴) |
16 | | cdlemc3.j |
. . . . . . . . 9
⊢ ∨ =
(join‘𝐾) |
17 | 7, 16, 8 | hlatjcl 33671 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
18 | 1, 6, 15, 17 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
19 | 7, 11 | lhpbase 34302 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
20 | 19 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → 𝑊 ∈ (Base‘𝐾)) |
21 | | cdlemc3.m |
. . . . . . . 8
⊢ ∧ =
(meet‘𝐾) |
22 | 7, 21 | latmcl 16875 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ (Base‘𝐾)) |
23 | 3, 18, 20, 22 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ (Base‘𝐾)) |
24 | | cdlemc3.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
25 | 7, 24, 16 | latlej1 16883 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑃) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ (Base‘𝐾)) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))) |
26 | 3, 14, 23, 25 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))) |
27 | | breq2 4587 |
. . . . 5
⊢ ((𝑄 ∨ (𝑅‘𝐹)) = ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) → ((𝐹‘𝑃) ≤ (𝑄 ∨ (𝑅‘𝐹)) ↔ (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)))) |
28 | 26, 27 | syl5ibrcom 236 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝑄 ∨ (𝑅‘𝐹)) = ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) → (𝐹‘𝑃) ≤ (𝑄 ∨ (𝑅‘𝐹)))) |
29 | | cdlemc3.r |
. . . . 5
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
30 | 24, 16, 21, 8, 11, 12, 29 | cdlemc3 34498 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝐹‘𝑃) ≤ (𝑄 ∨ (𝑅‘𝐹)) → 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃)))) |
31 | 28, 30 | syld 46 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → ((𝑄 ∨ (𝑅‘𝐹)) = ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)) → 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃)))) |
32 | 31 | necon3bd 2796 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) → (¬ 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃)) → (𝑄 ∨ (𝑅‘𝐹)) ≠ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊)))) |
33 | 32 | 3impia 1253 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ¬ 𝑄 ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑄 ∨ (𝑅‘𝐹)) ≠ ((𝐹‘𝑃) ∨ ((𝑃 ∨ 𝑄) ∧ 𝑊))) |