Proof of Theorem cdlemk48
Step | Hyp | Ref
| Expression |
1 | | simp11l 1283 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → 𝐾 ∈ HL) |
2 | 1 | hllatd 37386 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → 𝐾 ∈ Lat) |
3 | | simp11 1202 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
4 | | simp12 1203 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵))) |
5 | | simp13 1204 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) |
6 | | simp21 1205 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → 𝑁 ∈ 𝑇) |
7 | | simp22 1206 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
8 | | simp23 1207 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐹) = (𝑅‘𝑁)) |
9 | | cdlemk5.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐾) |
10 | | cdlemk5.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
11 | | cdlemk5.j |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
12 | | cdlemk5.m |
. . . . . . . 8
⊢ ∧ =
(meet‘𝐾) |
13 | | cdlemk5.a |
. . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) |
14 | | cdlemk5.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
15 | | cdlemk5.t |
. . . . . . . 8
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
16 | | cdlemk5.r |
. . . . . . . 8
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
17 | | cdlemk5.z |
. . . . . . . 8
⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) |
18 | | cdlemk5.y |
. . . . . . . 8
⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏)))) |
19 | | cdlemk5.x |
. . . . . . . 8
⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌)) |
20 | 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk35s 38959 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇) |
21 | 3, 4, 5, 6, 7, 8, 20 | syl132anc 1387 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇) |
22 | | simp3 1137 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) |
23 | 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19 | cdlemk35s 38959 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) |
24 | 3, 4, 22, 6, 7, 8,
23 | syl132anc 1387 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) |
25 | 14, 15 | ltrnco 38741 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇 ∧ ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) → (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋) ∈ 𝑇) |
26 | 3, 21, 24, 25 | syl3anc 1370 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋) ∈ 𝑇) |
27 | | simp22l 1291 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → 𝑃 ∈ 𝐴) |
28 | 10, 13, 14, 15 | ltrnat 38162 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋) ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐴) |
29 | 3, 26, 27, 28 | syl3anc 1370 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐴) |
30 | 9, 13 | atbase 37311 |
. . . 4
⊢
(((⦋𝐺
/ 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐴 → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐵) |
31 | 29, 30 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐵) |
32 | 9, 14, 15, 16 | trlcl 38186 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇) → (𝑅‘⦋𝐺 / 𝑔⦌𝑋) ∈ 𝐵) |
33 | 3, 21, 32 | syl2anc 584 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (𝑅‘⦋𝐺 / 𝑔⦌𝑋) ∈ 𝐵) |
34 | 9, 10, 11 | latlej1 18176 |
. . 3
⊢ ((𝐾 ∈ Lat ∧
((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐵 ∧ (𝑅‘⦋𝐺 / 𝑔⦌𝑋) ∈ 𝐵) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) |
35 | 2, 31, 33, 34 | syl3anc 1370 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) |
36 | 10, 11, 13, 14, 15, 16 | trlcoabs 38743 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇 ∧ ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋)) = ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) |
37 | 3, 21, 24, 7, 36 | syl121anc 1374 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋)) = ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) |
38 | 35, 37 | breqtrd 5099 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) |