Proof of Theorem cdleme35fnpq
Step | Hyp | Ref
| Expression |
1 | | simp3 1063 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) |
2 | | simp11 1091 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
3 | | simp12l 1174 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ∈ 𝐴) |
4 | | simp13l 1176 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑄 ∈ 𝐴) |
5 | | cdleme35.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
6 | | cdleme35.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
7 | | cdleme35.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
8 | | cdleme35.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
9 | | cdleme35.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
10 | | cdleme35.u |
. . . . . 6
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
11 | 5, 6, 7, 8, 9, 10 | cdlemeulpq 35507 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑈 ≤ (𝑃 ∨ 𝑄)) |
12 | 2, 3, 4, 11 | syl12anc 1324 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑈 ≤ (𝑃 ∨ 𝑄)) |
13 | | simp11l 1172 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝐾 ∈ HL) |
14 | | hllat 34650 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝐾 ∈ Lat) |
16 | | simp2rl 1130 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ∈ 𝐴) |
17 | | cdleme35.f |
. . . . . . . 8
⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊))) |
18 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
19 | 5, 6, 7, 8, 9, 10,
17, 18 | cdleme1b 35513 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐹 ∈ (Base‘𝐾)) |
20 | 2, 3, 4, 16, 19 | syl13anc 1328 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝐹 ∈ (Base‘𝐾)) |
21 | 5, 6, 7, 8, 9, 10,
18 | cdleme0aa 35497 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑈 ∈ (Base‘𝐾)) |
22 | 2, 3, 4, 21 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑈 ∈ (Base‘𝐾)) |
23 | 18, 6, 8 | hlatjcl 34653 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
24 | 13, 3, 4, 23 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
25 | 18, 5, 6 | latjle12 17062 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝐹 ≤ (𝑃 ∨ 𝑄) ∧ 𝑈 ≤ (𝑃 ∨ 𝑄)) ↔ (𝐹 ∨ 𝑈) ≤ (𝑃 ∨ 𝑄))) |
26 | 15, 20, 22, 24, 25 | syl13anc 1328 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝐹 ≤ (𝑃 ∨ 𝑄) ∧ 𝑈 ≤ (𝑃 ∨ 𝑄)) ↔ (𝐹 ∨ 𝑈) ≤ (𝑃 ∨ 𝑄))) |
27 | 26 | biimpd 219 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝐹 ≤ (𝑃 ∨ 𝑄) ∧ 𝑈 ≤ (𝑃 ∨ 𝑄)) → (𝐹 ∨ 𝑈) ≤ (𝑃 ∨ 𝑄))) |
28 | 12, 27 | mpan2d 710 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹 ≤ (𝑃 ∨ 𝑄) → (𝐹 ∨ 𝑈) ≤ (𝑃 ∨ 𝑄))) |
29 | 18, 8 | atbase 34576 |
. . . . . . 7
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾)) |
30 | 16, 29 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ∈ (Base‘𝐾)) |
31 | 18, 5, 6 | latlej1 17060 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → 𝑅 ≤ (𝑅 ∨ 𝑈)) |
32 | 15, 30, 22, 31 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ≤ (𝑅 ∨ 𝑈)) |
33 | 5, 6, 7, 8, 9, 10,
17 | cdleme35a 35736 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹 ∨ 𝑈) = (𝑅 ∨ 𝑈)) |
34 | 32, 33 | breqtrrd 4681 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑅 ≤ (𝐹 ∨ 𝑈)) |
35 | 18, 6 | latjcl 17051 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (𝐹 ∨ 𝑈) ∈ (Base‘𝐾)) |
36 | 15, 20, 22, 35 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹 ∨ 𝑈) ∈ (Base‘𝐾)) |
37 | 18, 5 | lattr 17056 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ (𝐹 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑅 ≤ (𝐹 ∨ 𝑈) ∧ (𝐹 ∨ 𝑈) ≤ (𝑃 ∨ 𝑄)) → 𝑅 ≤ (𝑃 ∨ 𝑄))) |
38 | 15, 30, 36, 24, 37 | syl13anc 1328 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑅 ≤ (𝐹 ∨ 𝑈) ∧ (𝐹 ∨ 𝑈) ≤ (𝑃 ∨ 𝑄)) → 𝑅 ≤ (𝑃 ∨ 𝑄))) |
39 | 34, 38 | mpand 711 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝐹 ∨ 𝑈) ≤ (𝑃 ∨ 𝑄) → 𝑅 ≤ (𝑃 ∨ 𝑄))) |
40 | 28, 39 | syld 47 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹 ≤ (𝑃 ∨ 𝑄) → 𝑅 ≤ (𝑃 ∨ 𝑄))) |
41 | 1, 40 | mtod 189 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝐹 ≤ (𝑃 ∨ 𝑄)) |