| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cdlemk1.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
cdlemk1.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
| 3 |
|
cdlemk1.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
| 4 |
|
cdlemk1.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
| 5 |
|
cdlemk1.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
| 6 |
|
cdlemk1.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
| 7 |
|
cdlemk1.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
| 8 |
|
cdlemk1.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
| 9 |
|
cdlemk1.s |
⊢ 𝑆 = ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑖 ∈ 𝑇 ( 𝑖 ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝑓 ) ) ∧ ( ( 𝑁 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑓 ∘ ◡ 𝐹 ) ) ) ) ) ) |
| 10 |
|
cdlemk1.o |
⊢ 𝑂 = ( 𝑆 ‘ 𝐷 ) |
| 11 |
|
simp11l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝐾 ∈ HL ) |
| 12 |
11
|
hllatd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝐾 ∈ Lat ) |
| 13 |
|
simp22l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝑃 ∈ 𝐴 ) |
| 14 |
|
simp1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ) |
| 15 |
|
simp211 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝑁 ∈ 𝑇 ) |
| 16 |
|
simp22 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) |
| 17 |
|
simp23 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) |
| 18 |
15 16 17
|
3jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑁 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ) |
| 19 |
|
simp3l1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) ) |
| 20 |
|
simp3l2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝐷 ≠ ( I ↾ 𝐵 ) ) |
| 21 |
|
simp3r1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ) |
| 22 |
19 20 21
|
3jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) |
| 23 |
1 2 3 4 5 6 7 8 9 10
|
cdlemkoatnle |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( 𝑁 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( ( 𝑂 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝑂 ‘ 𝑃 ) ≤ 𝑊 ) ) |
| 24 |
23
|
simpld |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( 𝑁 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑂 ‘ 𝑃 ) ∈ 𝐴 ) |
| 25 |
14 18 22 24
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑂 ‘ 𝑃 ) ∈ 𝐴 ) |
| 26 |
1 3 5
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝑂 ‘ 𝑃 ) ∈ 𝐴 ) → ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∈ 𝐵 ) |
| 27 |
11 13 25 26
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∈ 𝐵 ) |
| 28 |
|
simp11 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
| 29 |
|
simp212 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝐺 ∈ 𝑇 ) |
| 30 |
2 5 6 7
|
ltrnat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ) |
| 31 |
28 29 13 30
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ) |
| 32 |
|
simp13 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝐷 ∈ 𝑇 ) |
| 33 |
|
simp3r2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ) |
| 34 |
5 6 7 8
|
trlcocnvat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ∈ 𝐴 ) |
| 35 |
28 29 32 33 34
|
syl121anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ∈ 𝐴 ) |
| 36 |
1 3 5
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) |
| 37 |
11 31 35 36
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) |
| 38 |
1 4
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∈ 𝐵 ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ∈ 𝐵 ) |
| 39 |
12 27 37 38
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ∈ 𝐵 ) |
| 40 |
2 5 6 7
|
ltrnat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐷 ‘ 𝑃 ) ∈ 𝐴 ) |
| 41 |
28 32 13 40
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝐷 ‘ 𝑃 ) ∈ 𝐴 ) |
| 42 |
1 5 6 7 8
|
trlnidat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐷 ∈ 𝑇 ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ 𝐷 ) ∈ 𝐴 ) |
| 43 |
28 32 20 42
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑅 ‘ 𝐷 ) ∈ 𝐴 ) |
| 44 |
1 3 5
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐷 ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐷 ) ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∈ 𝐵 ) |
| 45 |
11 41 43 44
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∈ 𝐵 ) |
| 46 |
1 3 5
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐷 ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ∈ 𝐴 ) → ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) |
| 47 |
11 41 35 46
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) |
| 48 |
1 4
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) → ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ∈ 𝐵 ) |
| 49 |
12 45 47 48
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ∈ 𝐵 ) |
| 50 |
|
simp213 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝑋 ∈ 𝑇 ) |
| 51 |
2 5 6 7
|
ltrnat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ‘ 𝑃 ) ∈ 𝐴 ) |
| 52 |
28 50 13 51
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑋 ‘ 𝑃 ) ∈ 𝐴 ) |
| 53 |
|
simp3r3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) |
| 54 |
5 6 7 8
|
trlcocnvat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) → ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ∈ 𝐴 ) |
| 55 |
28 50 32 53 54
|
syl121anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ∈ 𝐴 ) |
| 56 |
1 3 5
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ‘ 𝑃 ) ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ∈ 𝐴 ) → ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) |
| 57 |
11 52 55 56
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) |
| 58 |
1 2 3 4 5 6 7 8 9 10
|
cdlemk1u |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( 𝑁 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ) ) → ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ≤ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ) |
| 59 |
14 18 22 58
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ≤ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ) |
| 60 |
1 2 4
|
latmlem1 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∈ 𝐵 ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ∈ 𝐵 ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ≤ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ≤ ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ) ) |
| 61 |
12 27 45 37 60
|
syl13anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ≤ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ≤ ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ) ) |
| 62 |
59 61
|
mpd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ≤ ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ) |
| 63 |
|
simp11r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝑊 ∈ 𝐻 ) |
| 64 |
1 2 3 5 6 7 8
|
cdlemk2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) = ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) |
| 65 |
11 63 32 29 16 64
|
syl221anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) = ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) |
| 66 |
65
|
oveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) = ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ) |
| 67 |
62 66
|
breqtrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ≤ ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ) |
| 68 |
|
simp3l3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) ) |
| 69 |
20 68
|
jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) |
| 70 |
1 2 3 5 6 7 8 4
|
cdlemk5a |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ≤ ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ) ) |
| 71 |
11 63 32 29 50 33 69 16 70
|
syl233anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐷 ) ) ∧ ( ( 𝐷 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ≤ ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ) ) |
| 72 |
1 2 12 39 49 57 67 71
|
lattrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐷 ∈ 𝑇 ) ∧ ( ( 𝑁 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( ( 𝑅 ‘ 𝐷 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐷 ) ∧ ( 𝑅 ‘ 𝑋 ) ≠ ( 𝑅 ‘ 𝐷 ) ) ) ) → ( ( 𝑃 ∨ ( 𝑂 ‘ 𝑃 ) ) ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐷 ) ) ) ) ≤ ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐷 ) ) ) ) |