Proof of Theorem cdlemk10
| Step | Hyp | Ref
| Expression |
| 1 | | cdlemk.v1 |
. 2
⊢ 𝑉 = (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) |
| 2 | | simp1 1137 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 3 | | simp22 1208 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐺 ∈ 𝑇) |
| 4 | | simp21 1207 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
| 5 | | cdlemk.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
| 6 | | cdlemk.t |
. . . . . . . . 9
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 7 | 5, 6 | ltrncnv 40148 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |
| 8 | 2, 4, 7 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ◡𝐹 ∈ 𝑇) |
| 9 | 5, 6 | ltrnco 40721 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝐺 ∘ ◡𝐹) ∈ 𝑇) |
| 10 | 2, 3, 8, 9 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺 ∘ ◡𝐹) ∈ 𝑇) |
| 11 | | cdlemk.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
| 12 | | cdlemk.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 13 | 11, 5, 6, 12 | trlle 40186 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ◡𝐹)) ≤ 𝑊) |
| 14 | 2, 10, 13 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ◡𝐹)) ≤ 𝑊) |
| 15 | | simp23 1209 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 ∈ 𝑇) |
| 16 | 5, 6 | ltrnco 40721 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝑋 ∘ ◡𝐹) ∈ 𝑇) |
| 17 | 2, 15, 8, 16 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ◡𝐹) ∈ 𝑇) |
| 18 | 11, 5, 6, 12 | trlle 40186 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ◡𝐹) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ◡𝐹)) ≤ 𝑊) |
| 19 | 2, 17, 18 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ◡𝐹)) ≤ 𝑊) |
| 20 | | simp1l 1198 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL) |
| 21 | 20 | hllatd 39365 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat) |
| 22 | | cdlemk.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
| 23 | 22, 5, 6, 12 | trlcl 40166 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐵) |
| 24 | 2, 10, 23 | syl2anc 584 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐵) |
| 25 | 22, 5, 6, 12 | trlcl 40166 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ◡𝐹) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ◡𝐹)) ∈ 𝐵) |
| 26 | 2, 17, 25 | syl2anc 584 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ◡𝐹)) ∈ 𝐵) |
| 27 | | simp1r 1199 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
| 28 | 22, 5 | lhpbase 40000 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
| 29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐵) |
| 30 | | cdlemk.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
| 31 | 22, 11, 30 | latjle12 18495 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋 ∘ ◡𝐹)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘(𝐺 ∘ ◡𝐹)) ≤ 𝑊 ∧ (𝑅‘(𝑋 ∘ ◡𝐹)) ≤ 𝑊) ↔ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ≤ 𝑊)) |
| 32 | 21, 24, 26, 29, 31 | syl13anc 1374 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑅‘(𝐺 ∘ ◡𝐹)) ≤ 𝑊 ∧ (𝑅‘(𝑋 ∘ ◡𝐹)) ≤ 𝑊) ↔ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ≤ 𝑊)) |
| 33 | 14, 19, 32 | mpbi2and 712 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ≤ 𝑊) |
| 34 | 22, 30 | latjcl 18484 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐵 ∧ (𝑅‘(𝑋 ∘ ◡𝐹)) ∈ 𝐵) → ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ∈ 𝐵) |
| 35 | 21, 24, 26, 34 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ∈ 𝐵) |
| 36 | | simp3l 1202 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴) |
| 37 | | cdlemk.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
| 38 | 11, 37, 5, 6 | ltrnat 40142 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴) |
| 39 | 2, 3, 36, 38 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐺‘𝑃) ∈ 𝐴) |
| 40 | 11, 37, 5, 6 | ltrnat 40142 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑋‘𝑃) ∈ 𝐴) |
| 41 | 2, 15, 36, 40 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐴) |
| 42 | 22, 30, 37 | hlatjcl 39368 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝐺‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) |
| 43 | 20, 39, 41, 42 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) |
| 44 | | cdlemk.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
| 45 | 22, 11, 44 | latmlem2 18515 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ ((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵)) → (((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ≤ 𝑊 → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) ≤ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))) |
| 46 | 21, 35, 29, 43, 45 | syl13anc 1374 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) ≤ 𝑊 → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) ≤ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))) |
| 47 | 33, 46 | mpd 15 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) ≤ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) |
| 48 | | simp3 1139 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
| 49 | 22, 11, 30, 37, 5, 6, 12, 44 | cdlemk9 40841 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ◡𝐺))) |
| 50 | 20, 27, 3, 15, 48, 49 | syl221anc 1383 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊) = (𝑅‘(𝑋 ∘ ◡𝐺))) |
| 51 | 47, 50 | breqtrd 5169 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) ≤ (𝑅‘(𝑋 ∘ ◡𝐺))) |
| 52 | 1, 51 | eqbrtrid 5178 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑉 ≤ (𝑅‘(𝑋 ∘ ◡𝐺))) |