Step | Hyp | Ref
| Expression |
1 | | ltrncnv.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | eqid 2738 |
. . . 4
⊢
((LDil‘𝐾)‘𝑊) = ((LDil‘𝐾)‘𝑊) |
3 | | ltrncnv.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
4 | 1, 2, 3 | ltrnldil 37781 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ ((LDil‘𝐾)‘𝑊)) |
5 | 1, 2 | ldilcnv 37774 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ ((LDil‘𝐾)‘𝑊)) → ◡𝐹 ∈ ((LDil‘𝐾)‘𝑊)) |
6 | 4, 5 | syldan 594 |
. 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 2738 |
. . . . . . . 8
⊢
(le‘𝐾) =
(le‘𝐾) |
13 | | eqid 2738 |
. . . . . . . 8
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
14 | 12, 13, 1, 3 | ltrncnvel 37801 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑝)(le‘𝐾)𝑊)) |
15 | 8, 9, 10, 11, 14 | syl112anc 1375 |
. . . . . 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 37801 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑞)(le‘𝐾)𝑊)) |
19 | 8, 9, 16, 17, 18 | syl112anc 1375 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑞)(le‘𝐾)𝑊)) |
20 | | eqid 2738 |
. . . . . . 7
⊢
(join‘𝐾) =
(join‘𝐾) |
21 | | eqid 2738 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
22 | 12, 20, 21, 13, 1, 3 | ltrnu 37780 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ ((◡𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑝)(le‘𝐾)𝑊) ∧ ((◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ ¬ (◡𝐹‘𝑞)(le‘𝐾)𝑊)) → (((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝)))(meet‘𝐾)𝑊) = (((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞)))(meet‘𝐾)𝑊)) |
23 | 7, 15, 19, 22 | syl3anc 1372 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝)))(meet‘𝐾)𝑊) = (((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞)))(meet‘𝐾)𝑊)) |
24 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
25 | 24, 1, 3 | ltrn1o 37783 |
. . . . . . . . . 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 36948 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ (Base‘𝐾)) |
28 | 10, 27 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑝 ∈ (Base‘𝐾)) |
29 | | f1ocnvfv2 7047 |
. . . . . . . . 9
⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾)) → (𝐹‘(◡𝐹‘𝑝)) = 𝑝) |
30 | 26, 28, 29 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐹‘(◡𝐹‘𝑝)) = 𝑝) |
31 | 30 | oveq2d 7188 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝))) = ((◡𝐹‘𝑝)(join‘𝐾)𝑝)) |
32 | | simp1ll 1237 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐾 ∈ HL) |
33 | 12, 13, 1, 3 | ltrncnvat 37800 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑝 ∈ (Atoms‘𝐾)) → (◡𝐹‘𝑝) ∈ (Atoms‘𝐾)) |
34 | 8, 9, 10, 33 | syl3anc 1372 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (◡𝐹‘𝑝) ∈ (Atoms‘𝐾)) |
35 | 20, 13 | hlatjcom 37027 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (◡𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((◡𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(◡𝐹‘𝑝))) |
36 | 32, 34, 10, 35 | syl3anc 1372 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(◡𝐹‘𝑝))) |
37 | 31, 36 | eqtrd 2773 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝))) = (𝑝(join‘𝐾)(◡𝐹‘𝑝))) |
38 | 37 | oveq1d 7187 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (((◡𝐹‘𝑝)(join‘𝐾)(𝐹‘(◡𝐹‘𝑝)))(meet‘𝐾)𝑊) = ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊)) |
39 | 24, 13 | atbase 36948 |
. . . . . . . . . 10
⊢ (𝑞 ∈ (Atoms‘𝐾) → 𝑞 ∈ (Base‘𝐾)) |
40 | 16, 39 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑞 ∈ (Base‘𝐾)) |
41 | | f1ocnvfv2 7047 |
. . . . . . . . 9
⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝐹‘(◡𝐹‘𝑞)) = 𝑞) |
42 | 26, 40, 41 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐹‘(◡𝐹‘𝑞)) = 𝑞) |
43 | 42 | oveq2d 7188 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞))) = ((◡𝐹‘𝑞)(join‘𝐾)𝑞)) |
44 | 12, 13, 1, 3 | ltrncnvat 37800 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑞 ∈ (Atoms‘𝐾)) → (◡𝐹‘𝑞) ∈ (Atoms‘𝐾)) |
45 | 8, 9, 16, 44 | syl3anc 1372 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (◡𝐹‘𝑞) ∈ (Atoms‘𝐾)) |
46 | 20, 13 | hlatjcom 37027 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (◡𝐹‘𝑞) ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) → ((◡𝐹‘𝑞)(join‘𝐾)𝑞) = (𝑞(join‘𝐾)(◡𝐹‘𝑞))) |
47 | 32, 45, 16, 46 | syl3anc 1372 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞)(join‘𝐾)𝑞) = (𝑞(join‘𝐾)(◡𝐹‘𝑞))) |
48 | 43, 47 | eqtrd 2773 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞))) = (𝑞(join‘𝐾)(◡𝐹‘𝑞))) |
49 | 48 | oveq1d 7187 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (((◡𝐹‘𝑞)(join‘𝐾)(𝐹‘(◡𝐹‘𝑞)))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊)) |
50 | 23, 38, 49 | 3eqtr3d 2781 |
. . . 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 3102 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊))) |
53 | 12, 20, 21, 13, 1, 2, 3 | isltrn 37778 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (◡𝐹 ∈ 𝑇 ↔ (◡𝐹 ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊))))) |
54 | 53 | adantr 484 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (◡𝐹 ∈ 𝑇 ↔ (◡𝐹 ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(◡𝐹‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(◡𝐹‘𝑞))(meet‘𝐾)𝑊))))) |
55 | 6, 52, 54 | mpbir2and 713 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |