Proof of Theorem cdlemk12
Step | Hyp | Ref
| Expression |
1 | | simp11l 1172 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐾 ∈ HL) |
2 | | simp22l 1180 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑃 ∈ 𝐴) |
3 | | simp11 1091 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
4 | | simp13 1093 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐺 ∈ 𝑇) |
5 | | cdlemk.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
6 | | cdlemk.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
7 | | cdlemk.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
8 | | cdlemk.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
9 | 5, 6, 7, 8 | ltrnat 35426 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴) |
10 | 3, 4, 2, 9 | syl3anc 1326 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝐺‘𝑃) ∈ 𝐴) |
11 | | simp12 1092 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐹 ∈ 𝑇) |
12 | | simp21r 1179 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑋 ∈ 𝑇) |
13 | 3, 11, 12 | 3jca 1242 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇)) |
14 | | simp21l 1178 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑁 ∈ 𝑇) |
15 | | simp22 1095 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
16 | | simp23 1096 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐹) = (𝑅‘𝑁)) |
17 | 14, 15, 16 | 3jca 1242 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) |
18 | | simp311 1208 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐹 ≠ ( I ↾ 𝐵)) |
19 | | simp313 1210 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑋 ≠ ( I ↾ 𝐵)) |
20 | | simp32r 1187 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝑋) ≠ (𝑅‘𝐹)) |
21 | | cdlemk.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
22 | | cdlemk.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
23 | | cdlemk.r |
. . . 4
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
24 | | cdlemk.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
25 | | cdlemk.s |
. . . 4
⊢ 𝑆 = (𝑓 ∈ 𝑇 ↦ (℩𝑖 ∈ 𝑇 (𝑖‘𝑃) = ((𝑃 ∨ (𝑅‘𝑓)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑓 ∘ ◡𝐹)))))) |
26 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 36134 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹))) → ((𝑆‘𝑋)‘𝑃) ∈ 𝐴) |
27 | 13, 17, 18, 19, 20, 26 | syl113anc 1338 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝑋)‘𝑃) ∈ 𝐴) |
28 | | simp33 1099 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≠ (𝑅‘𝑋)) |
29 | 28 | necomd 2849 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝑋) ≠ (𝑅‘𝐺)) |
30 | 6, 7, 8, 23 | trlcocnvat 36012 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐺)) → (𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐴) |
31 | 3, 12, 4, 29, 30 | syl121anc 1331 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐴) |
32 | | simp1 1061 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) |
33 | | simp312 1209 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐺 ≠ ( I ↾ 𝐵)) |
34 | | simp32l 1186 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≠ (𝑅‘𝐹)) |
35 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksat 36134 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹))) → ((𝑆‘𝐺)‘𝑃) ∈ 𝐴) |
36 | 32, 17, 18, 33, 34, 35 | syl113anc 1338 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ∈ 𝐴) |
37 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksv2 36135 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))) |
38 | 32, 17, 18, 33, 34, 37 | syl113anc 1338 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))) |
39 | | hllat 34650 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
40 | 1, 39 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐾 ∈ Lat) |
41 | 21, 6, 7, 8, 23 | trlnidat 35460 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ 𝐴) |
42 | 3, 4, 33, 41 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ∈ 𝐴) |
43 | 21, 22, 6 | hlatjcl 34653 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵) |
44 | 1, 2, 42, 43 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵) |
45 | 5, 6, 7, 8 | ltrnat 35426 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑁‘𝑃) ∈ 𝐴) |
46 | 3, 14, 2, 45 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑁‘𝑃) ∈ 𝐴) |
47 | 6, 7, 8, 23 | trlcocnvat 36012 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹)) → (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐴) |
48 | 3, 4, 11, 34, 47 | syl121anc 1331 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐴) |
49 | 21, 22, 6 | hlatjcl 34653 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑁‘𝑃) ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ◡𝐹)) ∈ 𝐴) → ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) ∈ 𝐵) |
50 | 1, 46, 48, 49 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) ∈ 𝐵) |
51 | 21, 5, 24 | latmle1 17076 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵 ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) ∈ 𝐵) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹)))) ≤ (𝑃 ∨ (𝑅‘𝐺))) |
52 | 40, 44, 50, 51 | syl3anc 1326 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹)))) ≤ (𝑃 ∨ (𝑅‘𝐺))) |
53 | 38, 52 | eqbrtrd 4675 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺))) |
54 | 5, 22, 6, 7, 8, 23 | trljat1 35453 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝐺)) = (𝑃 ∨ (𝐺‘𝑃))) |
55 | 3, 4, 15, 54 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∨ (𝑅‘𝐺)) = (𝑃 ∨ (𝐺‘𝑃))) |
56 | 53, 55 | breqtrd 4679 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝐺‘𝑃))) |
57 | | simp2 1062 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) |
58 | | simp31 1097 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵))) |
59 | | eqid 2622 |
. . . 4
⊢ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) = (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ◡𝐹)))) |
60 | 21, 5, 22, 6, 7, 8,
23, 24, 25, 59 | cdlemk11 36137 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹))) → ((𝑆‘𝐺)‘𝑃) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
61 | 32, 57, 58, 34, 20, 60 | syl113anc 1338 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
62 | 5, 22, 6 | hlatlej2 34662 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺))) |
63 | 1, 2, 42, 62 | syl3anc 1326 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺))) |
64 | 63, 55 | breqtrd 4679 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝐺‘𝑃))) |
65 | 21, 5, 22, 6, 7, 8,
23, 24, 25 | cdlemksel 36133 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹))) → (𝑆‘𝑋) ∈ 𝑇) |
66 | 13, 17, 18, 19, 20, 65 | syl113anc 1338 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑆‘𝑋) ∈ 𝑇) |
67 | 5, 6, 7, 8 | ltrnel 35425 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝑋) ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑆‘𝑋)‘𝑃) ≤ 𝑊)) |
68 | 3, 66, 15, 67 | syl3anc 1326 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑆‘𝑋)‘𝑃) ≤ 𝑊)) |
69 | 7, 8 | ltrncnv 35432 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → ◡𝐺 ∈ 𝑇) |
70 | 3, 4, 69 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ◡𝐺 ∈ 𝑇) |
71 | 7, 8, 23 | trlcnv 35452 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘◡𝐺) = (𝑅‘𝐺)) |
72 | 3, 4, 71 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘◡𝐺) = (𝑅‘𝐺)) |
73 | 72, 28 | eqnetrd 2861 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘◡𝐺) ≠ (𝑅‘𝑋)) |
74 | 21, 7, 8, 23 | trlcone 36016 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (◡𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ ((𝑅‘◡𝐺) ≠ (𝑅‘𝑋) ∧ 𝑋 ≠ ( I ↾ 𝐵))) → (𝑅‘◡𝐺) ≠ (𝑅‘(◡𝐺 ∘ 𝑋))) |
75 | 3, 70, 12, 73, 19, 74 | syl122anc 1335 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘◡𝐺) ≠ (𝑅‘(◡𝐺 ∘ 𝑋))) |
76 | 75 | necomd 2849 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(◡𝐺 ∘ 𝑋)) ≠ (𝑅‘◡𝐺)) |
77 | 7, 8 | ltrncom 36026 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ◡𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) → (◡𝐺 ∘ 𝑋) = (𝑋 ∘ ◡𝐺)) |
78 | 3, 70, 12, 77 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (◡𝐺 ∘ 𝑋) = (𝑋 ∘ ◡𝐺)) |
79 | 78 | fveq2d 6195 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(◡𝐺 ∘ 𝑋)) = (𝑅‘(𝑋 ∘ ◡𝐺))) |
80 | 76, 79, 72 | 3netr3d 2870 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝑋 ∘ ◡𝐺)) ≠ (𝑅‘𝐺)) |
81 | 7, 8 | ltrnco 36007 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ◡𝐺 ∈ 𝑇) → (𝑋 ∘ ◡𝐺) ∈ 𝑇) |
82 | 3, 12, 70, 81 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑋 ∘ ◡𝐺) ∈ 𝑇) |
83 | 5, 7, 8, 23 | trlle 35471 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ◡𝐺) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ◡𝐺)) ≤ 𝑊) |
84 | 3, 82, 83 | syl2anc 693 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝑋 ∘ ◡𝐺)) ≤ 𝑊) |
85 | 5, 7, 8, 23 | trlle 35471 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ≤ 𝑊) |
86 | 3, 4, 85 | syl2anc 693 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≤ 𝑊) |
87 | 5, 22, 6, 7 | lhp2atnle 35319 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑆‘𝑋)‘𝑃) ≤ 𝑊) ∧ (𝑅‘(𝑋 ∘ ◡𝐺)) ≠ (𝑅‘𝐺)) ∧ ((𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐴 ∧ (𝑅‘(𝑋 ∘ ◡𝐺)) ≤ 𝑊) ∧ ((𝑅‘𝐺) ∈ 𝐴 ∧ (𝑅‘𝐺) ≤ 𝑊)) → ¬ (𝑅‘𝐺) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
88 | 3, 68, 80, 31, 84, 42, 86, 87 | syl322anc 1354 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ¬ (𝑅‘𝐺) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
89 | | nbrne1 4672 |
. . 3
⊢ (((𝑅‘𝐺) ≤ (𝑃 ∨ (𝐺‘𝑃)) ∧ ¬ (𝑅‘𝐺) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) → (𝑃 ∨ (𝐺‘𝑃)) ≠ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
90 | 64, 88, 89 | syl2anc 693 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∨ (𝐺‘𝑃)) ≠ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺)))) |
91 | 5, 22, 24, 6 | 2atm 34813 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐺‘𝑃) ∈ 𝐴) ∧ (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ (𝑅‘(𝑋 ∘ ◡𝐺)) ∈ 𝐴 ∧ ((𝑆‘𝐺)‘𝑃) ∈ 𝐴) ∧ (((𝑆‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝐺‘𝑃)) ∧ ((𝑆‘𝐺)‘𝑃) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))) ∧ (𝑃 ∨ (𝐺‘𝑃)) ≠ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))))) |
92 | 1, 2, 10, 27, 31, 36, 56, 61, 90, 91 | syl333anc 1358 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ◡𝐺))))) |