Proof of Theorem cdlemk52
Step | Hyp | Ref
| Expression |
1 | | cdlemk5.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
2 | | cdlemk5.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | simp11l 1165 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝐾 ∈ HL) |
4 | | hllat 33668 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝐾 ∈ Lat) |
6 | | simp11 1084 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
7 | | simp12 1085 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵))) |
8 | | simp13 1086 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) |
9 | | simp21 1087 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝑁 ∈ 𝑇) |
10 | | simp22 1088 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
11 | | simp23 1089 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝑅‘𝐹) = (𝑅‘𝑁)) |
12 | | cdlemk5.j |
. . . . . . . . 9
⊢ ∨ =
(join‘𝐾) |
13 | | cdlemk5.m |
. . . . . . . . 9
⊢ ∧ =
(meet‘𝐾) |
14 | | cdlemk5.a |
. . . . . . . . 9
⊢ 𝐴 = (Atoms‘𝐾) |
15 | | cdlemk5.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
16 | | cdlemk5.t |
. . . . . . . . 9
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
17 | | cdlemk5.r |
. . . . . . . . 9
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
18 | | cdlemk5.z |
. . . . . . . . 9
⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) |
19 | | cdlemk5.y |
. . . . . . . . 9
⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ◡𝑏)))) |
20 | | cdlemk5.x |
. . . . . . . . 9
⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝑔)) → (𝑧‘𝑃) = 𝑌)) |
21 | 1, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdlemk35s 35243 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇) |
22 | 6, 7, 8, 9, 10, 11, 21 | syl132anc 1336 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇) |
23 | | simp31 1090 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝐼 ∈ 𝑇) |
24 | | simp32 1091 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝐼 ≠ ( I ↾ 𝐵)) |
25 | 23, 24 | jca 553 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) |
26 | 1, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdlemk35s 35243 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) |
27 | 6, 7, 25, 9, 10, 11, 26 | syl132anc 1336 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) |
28 | 15, 16 | ltrnco 35025 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇 ∧ ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) → (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋) ∈ 𝑇) |
29 | 6, 22, 27, 28 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋) ∈ 𝑇) |
30 | | simp22l 1173 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝑃 ∈ 𝐴) |
31 | 2, 14, 15, 16 | ltrnat 34444 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋) ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐴) |
32 | 6, 29, 30, 31 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐴) |
33 | 1, 14 | atbase 33594 |
. . . . 5
⊢
(((⦋𝐺
/ 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐴 → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐵) |
34 | 32, 33 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐵) |
35 | 2, 14, 15, 16 | ltrnat 34444 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∈ 𝐴) |
36 | 6, 22, 30, 35 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∈ 𝐴) |
37 | 1, 14 | atbase 33594 |
. . . . . . 7
⊢
((⦋𝐺 /
𝑔⦌𝑋‘𝑃) ∈ 𝐴 → (⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∈ 𝐵) |
38 | 36, 37 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∈ 𝐵) |
39 | 1, 15, 16, 17 | trlcl 34469 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇) → (𝑅‘⦋𝐼 / 𝑔⦌𝑋) ∈ 𝐵) |
40 | 6, 27, 39 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝑅‘⦋𝐼 / 𝑔⦌𝑋) ∈ 𝐵) |
41 | 1, 12 | latjcl 16874 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧
(⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∈ 𝐵 ∧ (𝑅‘⦋𝐼 / 𝑔⦌𝑋) ∈ 𝐵) → ((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∈ 𝐵) |
42 | 5, 38, 40, 41 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∈ 𝐵) |
43 | 2, 14, 15, 16 | ltrnat 34444 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋𝐼 / 𝑔⦌𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∈ 𝐴) |
44 | 6, 27, 30, 43 | syl3anc 1318 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∈ 𝐴) |
45 | 1, 14 | atbase 33594 |
. . . . . . 7
⊢
((⦋𝐼 /
𝑔⦌𝑋‘𝑃) ∈ 𝐴 → (⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∈ 𝐵) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∈ 𝐵) |
47 | 1, 15, 16, 17 | trlcl 34469 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋𝐺 / 𝑔⦌𝑋 ∈ 𝑇) → (𝑅‘⦋𝐺 / 𝑔⦌𝑋) ∈ 𝐵) |
48 | 6, 22, 47 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝑅‘⦋𝐺 / 𝑔⦌𝑋) ∈ 𝐵) |
49 | 1, 12 | latjcl 16874 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧
(⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∈ 𝐵 ∧ (𝑅‘⦋𝐺 / 𝑔⦌𝑋) ∈ 𝐵) → ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋)) ∈ 𝐵) |
50 | 5, 46, 48, 49 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋)) ∈ 𝐵) |
51 | 1, 13 | latmcl 16875 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧
((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∈ 𝐵 ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋)) ∈ 𝐵) → (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) ∈ 𝐵) |
52 | 5, 42, 50, 51 | syl3anc 1318 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) ∈ 𝐵) |
53 | | simp11r 1166 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝑊 ∈ 𝐻) |
54 | 1, 14, 15, 16, 17 | trlnidat 34478 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐼) ∈ 𝐴) |
55 | 3, 53, 23, 24, 54 | syl211anc 1324 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝑅‘𝐼) ∈ 𝐴) |
56 | 1, 12, 14 | hlatjcl 33671 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧
(⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∈ 𝐴 ∧ (𝑅‘𝐼) ∈ 𝐴) → ((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∈ 𝐵) |
57 | 3, 36, 55, 56 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∈ 𝐵) |
58 | | simp13l 1169 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝐺 ∈ 𝑇) |
59 | | simp13r 1170 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝐺 ≠ ( I ↾ 𝐵)) |
60 | 1, 14, 15, 16, 17 | trlnidat 34478 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ 𝐴) |
61 | 3, 53, 58, 59, 60 | syl211anc 1324 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝑅‘𝐺) ∈ 𝐴) |
62 | 1, 12, 14 | hlatjcl 33671 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧
(⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺)) ∈ 𝐵) |
63 | 3, 44, 61, 62 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺)) ∈ 𝐵) |
64 | 1, 13 | latmcl 16875 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧
((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∈ 𝐵 ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺)) ∈ 𝐵) → (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺))) ∈ 𝐵) |
65 | 5, 57, 63, 64 | syl3anc 1318 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺))) ∈ 𝐵) |
66 | 1, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdlemk50 35258 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋)))) |
67 | 25, 66 | syld3an3 1363 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋)))) |
68 | 1, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdlemk51 35259 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵))) → (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) ≤ (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺)))) |
69 | 25, 68 | syld3an3 1363 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐼 / 𝑔⦌𝑋)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘⦋𝐺 / 𝑔⦌𝑋))) ≤ (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺)))) |
70 | 1, 2, 5, 34, 52, 65, 67, 69 | lattrd 16881 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺)))) |
71 | 1, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdlemk47 35255 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃) = (((⦋𝐺 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐼)) ∧ ((⦋𝐼 / 𝑔⦌𝑋‘𝑃) ∨ (𝑅‘𝐺)))) |
72 | 70, 71 | breqtrrd 4611 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃)) |
73 | | hlatl 33665 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
74 | 3, 73 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → 𝐾 ∈ AtLat) |
75 | 15, 16 | ltrnco 35025 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) → (𝐺 ∘ 𝐼) ∈ 𝑇) |
76 | 6, 58, 23, 75 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝐺 ∘ 𝐼) ∈ 𝑇) |
77 | 58, 23 | jca 553 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇)) |
78 | | simp33 1092 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝑅‘𝐺) ≠ (𝑅‘𝐼)) |
79 | 1, 15, 16, 17 | trlconid 35031 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝐼 ∈ 𝑇) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼)) → (𝐺 ∘ 𝐼) ≠ ( I ↾ 𝐵)) |
80 | 6, 77, 78, 79 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (𝐺 ∘ 𝐼) ≠ ( I ↾ 𝐵)) |
81 | 76, 80 | jca 553 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((𝐺 ∘ 𝐼) ∈ 𝑇 ∧ (𝐺 ∘ 𝐼) ≠ ( I ↾ 𝐵))) |
82 | 1, 2, 12, 13, 14, 15, 16, 17, 18, 19, 20 | cdlemk35s 35243 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ ((𝐺 ∘ 𝐼) ∈ 𝑇 ∧ (𝐺 ∘ 𝐼) ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → ⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋 ∈ 𝑇) |
83 | 6, 7, 81, 9, 10, 11, 82 | syl132anc 1336 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋 ∈ 𝑇) |
84 | 2, 14, 15, 16 | ltrnat 34444 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃) ∈ 𝐴) |
85 | 6, 83, 30, 84 | syl3anc 1318 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃) ∈ 𝐴) |
86 | 2, 14 | atcmp 33616 |
. . 3
⊢ ((𝐾 ∈ AtLat ∧
((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ∈ 𝐴 ∧ (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃) ∈ 𝐴) → (((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃) ↔ ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) = (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃))) |
87 | 74, 32, 85, 86 | syl3anc 1318 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → (((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) ≤ (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃) ↔ ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) = (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃))) |
88 | 72, 87 | mpbid 221 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵))) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐼 ∈ 𝑇 ∧ 𝐼 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐼))) → ((⦋𝐺 / 𝑔⦌𝑋 ∘ ⦋𝐼 / 𝑔⦌𝑋)‘𝑃) = (⦋(𝐺 ∘ 𝐼) / 𝑔⦌𝑋‘𝑃)) |