Proof of Theorem cdlemk4
Step | Hyp | Ref
| Expression |
1 | | simp1l 1078 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL) |
2 | | simp1 1054 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
3 | | simp2l 1080 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
4 | | simp3l 1082 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴) |
5 | | cdlemk.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
6 | | cdlemk.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
7 | | cdlemk.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
8 | | cdlemk.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
9 | 5, 6, 7, 8 | ltrnat 34444 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
10 | 2, 3, 4, 9 | syl3anc 1318 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐴) |
11 | | simp2r 1081 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 ∈ 𝑇) |
12 | 5, 6, 7, 8 | ltrnat 34444 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑋‘𝑃) ∈ 𝐴) |
13 | 2, 11, 4, 12 | syl3anc 1318 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐴) |
14 | | cdlemk.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
15 | 5, 14, 6 | hlatlej1 33679 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) |
16 | 1, 10, 13, 15 | syl3anc 1318 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) |
17 | | hllat 33668 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
18 | 1, 17 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat) |
19 | | cdlemk.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
20 | 19, 6 | atbase 33594 |
. . . . . 6
⊢ ((𝐹‘𝑃) ∈ 𝐴 → (𝐹‘𝑃) ∈ 𝐵) |
21 | 10, 20 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐵) |
22 | 19, 6 | atbase 33594 |
. . . . . 6
⊢ ((𝑋‘𝑃) ∈ 𝐴 → (𝑋‘𝑃) ∈ 𝐵) |
23 | 13, 22 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ∈ 𝐵) |
24 | 19, 14 | latjcl 16874 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑃) ∈ 𝐵 ∧ (𝑋‘𝑃) ∈ 𝐵) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) |
25 | 18, 21, 23, 24 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) |
26 | | simp1r 1079 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻) |
27 | 19, 7 | lhpbase 34302 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐵) |
29 | 5, 14, 6 | hlatlej2 33680 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝑋‘𝑃) ∈ 𝐴) → (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) |
30 | 1, 10, 13, 29 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) |
31 | | cdlemk.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
32 | 19, 5, 14, 31, 6 | atmod3i1 34168 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ((𝑋‘𝑃) ∈ 𝐴 ∧ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ (𝑋‘𝑃) ≤ ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) → ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊))) |
33 | 1, 13, 25, 28, 30, 32 | syl131anc 1331 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊))) |
34 | 7, 8 | ltrncnv 34450 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |
35 | 2, 3, 34 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ◡𝐹 ∈ 𝑇) |
36 | 7, 8 | ltrnco 35025 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ◡𝐹 ∈ 𝑇) → (𝑋 ∘ ◡𝐹) ∈ 𝑇) |
37 | 2, 11, 35, 36 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ◡𝐹) ∈ 𝑇) |
38 | 5, 6, 7, 8 | ltrnel 34443 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) |
39 | 3, 38 | syld3an2 1365 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) |
40 | | cdlemk.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
41 | 5, 14, 31, 6, 7, 8,
40 | trlval2 34468 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ◡𝐹) ∈ 𝑇 ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊)) |
42 | 2, 37, 39, 41 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ◡𝐹)) = (((𝐹‘𝑃) ∨ ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊)) |
43 | 19, 7, 8 | ltrn1o 34428 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵) |
44 | 2, 3, 43 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹:𝐵–1-1-onto→𝐵) |
45 | | f1ococnv1 6078 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐵–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐵)) |
47 | 46 | coeq2d 5206 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ (◡𝐹 ∘ 𝐹)) = (𝑋 ∘ ( I ↾ 𝐵))) |
48 | 19, 7, 8 | ltrn1o 34428 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇) → 𝑋:𝐵–1-1-onto→𝐵) |
49 | 2, 11, 48 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋:𝐵–1-1-onto→𝐵) |
50 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ (𝑋:𝐵–1-1-onto→𝐵 → 𝑋:𝐵⟶𝐵) |
51 | | fcoi1 5991 |
. . . . . . . . . . . . 13
⊢ (𝑋:𝐵⟶𝐵 → (𝑋 ∘ ( I ↾ 𝐵)) = 𝑋) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋 ∘ ( I ↾ 𝐵)) = 𝑋) |
53 | 47, 52 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 = (𝑋 ∘ (◡𝐹 ∘ 𝐹))) |
54 | | coass 5571 |
. . . . . . . . . . 11
⊢ ((𝑋 ∘ ◡𝐹) ∘ 𝐹) = (𝑋 ∘ (◡𝐹 ∘ 𝐹)) |
55 | 53, 54 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑋 = ((𝑋 ∘ ◡𝐹) ∘ 𝐹)) |
56 | 55 | fveq1d 6105 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) = (((𝑋 ∘ ◡𝐹) ∘ 𝐹)‘𝑃)) |
57 | 5, 6, 7, 8 | ltrncoval 34449 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∘ ◡𝐹) ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ 𝑃 ∈ 𝐴) → (((𝑋 ∘ ◡𝐹) ∘ 𝐹)‘𝑃) = ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃))) |
58 | 2, 37, 3, 4, 57 | syl121anc 1323 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑋 ∘ ◡𝐹) ∘ 𝐹)‘𝑃) = ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃))) |
59 | 56, 58 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑋‘𝑃) = ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃))) |
60 | 59 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = ((𝐹‘𝑃) ∨ ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃)))) |
61 | 60 | eqcomd 2616 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃))) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) |
62 | 61 | oveq1d 6564 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ ((𝑋 ∘ ◡𝐹)‘(𝐹‘𝑃))) ∧ 𝑊) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) |
63 | 42, 62 | eqtrd 2644 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝑋 ∘ ◡𝐹)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊)) |
64 | 63 | oveq2d 6565 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐹))) = ((𝑋‘𝑃) ∨ (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ 𝑊))) |
65 | 5, 6, 7, 8 | ltrnel 34443 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊)) |
66 | 11, 65 | syld3an2 1365 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊)) |
67 | | eqid 2610 |
. . . . . . 7
⊢
(1.‘𝐾) =
(1.‘𝐾) |
68 | 5, 14, 67, 6, 7 | lhpjat2 34325 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋‘𝑃) ∈ 𝐴 ∧ ¬ (𝑋‘𝑃) ≤ 𝑊)) → ((𝑋‘𝑃) ∨ 𝑊) = (1.‘𝐾)) |
69 | 2, 66, 68 | syl2anc 691 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑋‘𝑃) ∨ 𝑊) = (1.‘𝐾)) |
70 | 69 | oveq2d 6565 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾))) |
71 | | hlol 33666 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
72 | 1, 71 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ OL) |
73 | 19, 31, 67 | olm11 33532 |
. . . . 5
⊢ ((𝐾 ∈ OL ∧ ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∈ 𝐵) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) |
74 | 72, 25, 73 | syl2anc 691 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ (1.‘𝐾)) = ((𝐹‘𝑃) ∨ (𝑋‘𝑃))) |
75 | 70, 74 | eqtr2d 2645 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = (((𝐹‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑋‘𝑃) ∨ 𝑊))) |
76 | 33, 64, 75 | 3eqtr4rd 2655 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑋‘𝑃)) = ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) |
77 | 16, 76 | breqtrd 4609 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ≤ ((𝑋‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) |