| Step | Hyp | Ref
| Expression |
| 1 | | ltrncnv.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
| 2 | | eqid 2737 |
. . . 4
⊢
((LDil‘𝐾)‘𝑊) = ((LDil‘𝐾)‘𝑊) |
| 3 | | ltrncnv.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 4 | 1, 2, 3 | ltrnldil 40124 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ ((LDil‘𝐾)‘𝑊)) |
| 5 | 1, 2 | ldilcnv 40117 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ ((LDil‘𝐾)‘𝑊)) → ◡𝐹 ∈ ((LDil‘𝐾)‘𝑊)) |
| 6 | 4, 5 | syldan 591 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ ((LDil‘𝐾)‘𝑊)) |
| 7 | | simp1 1137 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇)) |
| 8 | | simp1l 1198 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 9 | | simp1r 1199 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐹 ∈ 𝑇) |
| 10 | | simp2l 1200 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑝 ∈ (Atoms‘𝐾)) |
| 11 | | simp3l 1202 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑝(le‘𝐾)𝑊) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢
(le‘𝐾) =
(le‘𝐾) |
| 13 | | eqid 2737 |
. . . . . . . 8
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
| 14 | 12, 13, 1, 3 | ltrncnvel 40144 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑝)(le‘𝐾)𝑊)) |
| 15 | 8, 9, 10, 11, 14 | syl112anc 1376 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑝)(le‘𝐾)𝑊)) |
| 16 | | simp2r 1201 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑞 ∈ (Atoms‘𝐾)) |
| 17 | | simp3r 1203 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑞(le‘𝐾)𝑊) |
| 18 | 12, 13, 1, 3 | ltrncnvel 40144 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑞)(le‘𝐾)𝑊)) |
| 19 | 8, 9, 16, 17, 18 | syl112anc 1376 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑞)(le‘𝐾)𝑊)) |
| 20 | | eqid 2737 |
. . . . . . 7
⊢
(join‘𝐾) =
(join‘𝐾) |
| 21 | | eqid 2737 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
| 22 | 12, 20, 21, 13, 1, 3 | ltrnu 40123 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ((◡𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑝)(le‘𝐾)𝑊) ∧ ((◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑞)(le‘𝐾)𝑊)) → (((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝)))(meet‘𝐾)𝑊) = (((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞)))(meet‘𝐾)𝑊)) |
| 23 | 7, 15, 19, 22 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝)))(meet‘𝐾)𝑊) = (((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞)))(meet‘𝐾)𝑊)) |
| 24 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 25 | 24, 1, 3 | ltrn1o 40126 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) |
| 26 | 25 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) |
| 27 | 24, 13 | atbase 39290 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ (Base‘𝐾)) |
| 28 | 10, 27 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑝 ∈ (Base‘𝐾)) |
| 29 | | f1ocnvfv2 7297 |
. . . . . . . . 9
⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾)) → (𝐹‘(◡𝐹‘𝑝)) = 𝑝) |
| 30 | 26, 28, 29 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐹‘(◡𝐹‘𝑝)) = 𝑝) |
| 31 | 30 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝))) = ((◡𝐹‘𝑝)(join‘𝐾)𝑝)) |
| 32 | | simp1ll 1237 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐾 ∈ HL) |
| 33 | 12, 13, 1, 3 | ltrncnvat 40143 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑝 ∈ (Atoms‘𝐾)) → (◡𝐹‘𝑝) ∈ (Atoms‘𝐾)) |
| 34 | 8, 9, 10, 33 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (◡𝐹‘𝑝) ∈ (Atoms‘𝐾)) |
| 35 | 20, 13 | hlatjcom 39369 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (◡𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((◡𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(◡𝐹‘𝑝))) |
| 36 | 32, 34, 10, 35 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(◡𝐹‘𝑝))) |
| 37 | 31, 36 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝))) = (𝑝(join‘𝐾)(◡𝐹‘𝑝))) |
| 38 | 37 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝)))(meet‘𝐾)𝑊) = ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊)) |
| 39 | 24, 13 | atbase 39290 |
. . . . . . . . . 10
⊢ (𝑞 ∈ (Atoms‘𝐾) → 𝑞 ∈ (Base‘𝐾)) |
| 40 | 16, 39 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑞 ∈ (Base‘𝐾)) |
| 41 | | f1ocnvfv2 7297 |
. . . . . . . . 9
⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝐹‘(◡𝐹‘𝑞)) = 𝑞) |
| 42 | 26, 40, 41 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐹‘(◡𝐹‘𝑞)) = 𝑞) |
| 43 | 42 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞))) = ((◡𝐹‘𝑞)(join‘𝐾)𝑞)) |
| 44 | 12, 13, 1, 3 | ltrncnvat 40143 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑞 ∈ (Atoms‘𝐾)) → (◡𝐹‘𝑞) ∈ (Atoms‘𝐾)) |
| 45 | 8, 9, 16, 44 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (◡𝐹‘𝑞) ∈ (Atoms‘𝐾)) |
| 46 | 20, 13 | hlatjcom 39369 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) → ((◡𝐹‘𝑞)(join‘𝐾)𝑞) = (𝑞(join‘𝐾)(◡𝐹‘𝑞))) |
| 47 | 32, 45, 16, 46 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞)(join‘𝐾)𝑞) = (𝑞(join‘𝐾)(◡𝐹‘𝑞))) |
| 48 | 43, 47 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞))) = (𝑞(join‘𝐾)(◡𝐹‘𝑞))) |
| 49 | 48 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞)))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊)) |
| 50 | 23, 38, 49 | 3eqtr3d 2785 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊)) |
| 51 | 50 | 3exp 1120 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) → ((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊)))) |
| 52 | 51 | ralrimivv 3200 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊))) |
| 53 | 12, 20, 21, 13, 1, 2, 3 | isltrn 40121 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (◡𝐹 ∈ 𝑇 ↔ (◡𝐹 ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊))))) |
| 54 | 53 | adantr 480 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (◡𝐹 ∈ 𝑇 ↔ (◡𝐹 ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊))))) |
| 55 | 6, 52, 54 | mpbir2and 713 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |