Proof of Theorem cdlemg42
| Step | Hyp | Ref
| Expression |
| 1 | | simp33 1212 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ≠ (𝑅‘𝐺)) |
| 2 | | simpl1l 1225 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝐾 ∈ HL) |
| 3 | | simp31l 1297 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐴) |
| 4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝑃 ∈ 𝐴) |
| 5 | | simp1 1137 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 6 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇) |
| 7 | | cdlemg42.l |
. . . . . . . . . . . 12
⊢ ≤ =
(le‘𝐾) |
| 8 | | cdlemg42.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (Atoms‘𝐾) |
| 9 | | cdlemg42.h |
. . . . . . . . . . . 12
⊢ 𝐻 = (LHyp‘𝐾) |
| 10 | | cdlemg42.t |
. . . . . . . . . . . 12
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 11 | 7, 8, 9, 10 | ltrnat 40142 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
| 12 | 5, 6, 3, 11 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐹‘𝑃) ∈ 𝐴) |
| 13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝐹‘𝑃) ∈ 𝐴) |
| 14 | | cdlemg42.j |
. . . . . . . . . 10
⊢ ∨ =
(join‘𝐾) |
| 15 | 7, 14, 8 | hlatlej1 39376 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ (𝐹‘𝑃))) |
| 16 | 2, 4, 13, 15 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝑃 ≤ (𝑃 ∨ (𝐹‘𝑃))) |
| 17 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) |
| 18 | 2 | hllatd 39365 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝐾 ∈ Lat) |
| 19 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 20 | 19, 8 | atbase 39290 |
. . . . . . . . . 10
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
| 21 | 4, 20 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝑃 ∈ (Base‘𝐾)) |
| 22 | | simp2r 1201 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇) |
| 23 | 7, 8, 9, 10 | ltrnat 40142 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴) |
| 24 | 5, 22, 3, 23 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺‘𝑃) ∈ 𝐴) |
| 25 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝐺‘𝑃) ∈ 𝐴) |
| 26 | 19, 8 | atbase 39290 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑃) ∈ 𝐴 → (𝐺‘𝑃) ∈ (Base‘𝐾)) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝐺‘𝑃) ∈ (Base‘𝐾)) |
| 28 | 19, 14, 8 | hlatjcl 39368 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾)) |
| 29 | 2, 4, 13, 28 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾)) |
| 30 | 19, 7, 14 | latjle12 18495 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ (𝐺‘𝑃) ∈ (Base‘𝐾) ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑃 ∨ (𝐹‘𝑃)) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ (𝐹‘𝑃)))) |
| 31 | 18, 21, 27, 29, 30 | syl13anc 1374 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → ((𝑃 ≤ (𝑃 ∨ (𝐹‘𝑃)) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ (𝐹‘𝑃)))) |
| 32 | 16, 17, 31 | mpbi2and 712 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ (𝐹‘𝑃))) |
| 33 | | simpl32 1256 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝐺‘𝑃) ≠ 𝑃) |
| 34 | 33 | necomd 2996 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝑃 ≠ (𝐺‘𝑃)) |
| 35 | 7, 14, 8 | ps-1 39479 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝐺‘𝑃) ∈ 𝐴 ∧ 𝑃 ≠ (𝐺‘𝑃)) ∧ (𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴)) → ((𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ (𝐹‘𝑃)) ↔ (𝑃 ∨ (𝐺‘𝑃)) = (𝑃 ∨ (𝐹‘𝑃)))) |
| 36 | 2, 4, 25, 34, 4, 13, 35 | syl132anc 1390 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → ((𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ (𝐹‘𝑃)) ↔ (𝑃 ∨ (𝐺‘𝑃)) = (𝑃 ∨ (𝐹‘𝑃)))) |
| 37 | 32, 36 | mpbid 232 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑃 ∨ (𝐺‘𝑃)) = (𝑃 ∨ (𝐹‘𝑃))) |
| 38 | 37 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → ((𝑃 ∨ (𝐺‘𝑃))(meet‘𝐾)𝑊) = ((𝑃 ∨ (𝐹‘𝑃))(meet‘𝐾)𝑊)) |
| 39 | | simpl1 1192 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 40 | | simpl2r 1228 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝐺 ∈ 𝑇) |
| 41 | | simpl31 1255 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
| 42 | | eqid 2737 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
| 43 | | cdlemg42.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 44 | 7, 14, 42, 8, 9, 10, 43 | trlval2 40165 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃))(meet‘𝐾)𝑊)) |
| 45 | 39, 40, 41, 44 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃))(meet‘𝐾)𝑊)) |
| 46 | | simpl2l 1227 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → 𝐹 ∈ 𝑇) |
| 47 | 7, 14, 42, 8, 9, 10, 43 | trlval2 40165 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃))(meet‘𝐾)𝑊)) |
| 48 | 39, 46, 41, 47 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃))(meet‘𝐾)𝑊)) |
| 49 | 38, 45, 48 | 3eqtr4rd 2788 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑅‘𝐹) = (𝑅‘𝐺)) |
| 50 | 49 | ex 412 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃)) → (𝑅‘𝐹) = (𝑅‘𝐺))) |
| 51 | 50 | necon3ad 2953 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑅‘𝐹) ≠ (𝑅‘𝐺) → ¬ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃)))) |
| 52 | 1, 51 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) |