Proof of Theorem cdleme42i
Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝐾 ∈ HL) |
2 | 1 | hllatd 37034 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝐾 ∈ Lat) |
3 | | simp1 1137 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))) |
4 | | simp2ll 1241 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝑅 ∈ 𝐴) |
5 | | cdleme41.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
6 | | cdleme41.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
7 | 5, 6 | atbase 36959 |
. . . . 5
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵) |
8 | 4, 7 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝑅 ∈ 𝐵) |
9 | | cdleme41.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
10 | | cdleme41.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
11 | | cdleme41.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
12 | | cdleme41.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
13 | | cdleme41.u |
. . . . 5
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
14 | | cdleme41.d |
. . . . 5
⊢ 𝐷 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) |
15 | | cdleme41.e |
. . . . 5
⊢ 𝐸 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊))) |
16 | | cdleme41.g |
. . . . 5
⊢ 𝐺 = ((𝑃 ∨ 𝑄) ∧ (𝐸 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊))) |
17 | | cdleme41.i |
. . . . 5
⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) |
18 | | cdleme41.n |
. . . . 5
⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐷) |
19 | | cdleme41.o |
. . . . 5
⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊)))) |
20 | | cdleme41.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥)) |
21 | 5, 9, 10, 11, 6, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdleme32fvcl 38110 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑅 ∈ 𝐵) → (𝐹‘𝑅) ∈ 𝐵) |
22 | 3, 8, 21 | syl2anc 587 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘𝑅) ∈ 𝐵) |
23 | | cdleme34e.v |
. . . 4
⊢ 𝑉 = ((𝑅 ∨ 𝑆) ∧ 𝑊) |
24 | | simp2rl 1243 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝑆 ∈ 𝐴) |
25 | 5, 10, 6 | hlatjcl 37037 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ 𝐵) |
26 | 1, 4, 24, 25 | syl3anc 1372 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝑅 ∨ 𝑆) ∈ 𝐵) |
27 | | simp11r 1286 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝑊 ∈ 𝐻) |
28 | 5, 12 | lhpbase 37668 |
. . . . . 6
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
29 | 27, 28 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝑊 ∈ 𝐵) |
30 | 5, 11 | latmcl 17791 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑆) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐵) |
31 | 2, 26, 29, 30 | syl3anc 1372 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ((𝑅 ∨ 𝑆) ∧ 𝑊) ∈ 𝐵) |
32 | 23, 31 | eqeltrid 2838 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝑉 ∈ 𝐵) |
33 | 5, 9, 10 | latlej1 17799 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑅) ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘𝑅) ≤ ((𝐹‘𝑅) ∨ 𝑉)) |
34 | 2, 22, 32, 33 | syl3anc 1372 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘𝑅) ≤ ((𝐹‘𝑅) ∨ 𝑉)) |
35 | 5, 9, 10, 11, 6, 12, 13, 14, 15, 16, 17, 18, 19, 20, 23 | cdleme42h 38152 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘𝑆) ≤ ((𝐹‘𝑅) ∨ 𝑉)) |
36 | 5, 6 | atbase 36959 |
. . . . 5
⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ 𝐵) |
37 | 24, 36 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → 𝑆 ∈ 𝐵) |
38 | 5, 9, 10, 11, 6, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdleme32fvcl 38110 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑆 ∈ 𝐵) → (𝐹‘𝑆) ∈ 𝐵) |
39 | 3, 37, 38 | syl2anc 587 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (𝐹‘𝑆) ∈ 𝐵) |
40 | 5, 10 | latjcl 17790 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑅) ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑅) ∨ 𝑉) ∈ 𝐵) |
41 | 2, 22, 32, 40 | syl3anc 1372 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ((𝐹‘𝑅) ∨ 𝑉) ∈ 𝐵) |
42 | 5, 9, 10 | latjle12 17801 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ ((𝐹‘𝑅) ∈ 𝐵 ∧ (𝐹‘𝑆) ∈ 𝐵 ∧ ((𝐹‘𝑅) ∨ 𝑉) ∈ 𝐵)) → (((𝐹‘𝑅) ≤ ((𝐹‘𝑅) ∨ 𝑉) ∧ (𝐹‘𝑆) ≤ ((𝐹‘𝑅) ∨ 𝑉)) ↔ ((𝐹‘𝑅) ∨ (𝐹‘𝑆)) ≤ ((𝐹‘𝑅) ∨ 𝑉))) |
43 | 2, 22, 39, 41, 42 | syl13anc 1373 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → (((𝐹‘𝑅) ≤ ((𝐹‘𝑅) ∨ 𝑉) ∧ (𝐹‘𝑆) ≤ ((𝐹‘𝑅) ∨ 𝑉)) ↔ ((𝐹‘𝑅) ∨ (𝐹‘𝑆)) ≤ ((𝐹‘𝑅) ∨ 𝑉))) |
44 | 34, 35, 43 | mpbi2and 712 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ((𝐹‘𝑅) ∨ (𝐹‘𝑆)) ≤ ((𝐹‘𝑅) ∨ 𝑉)) |