Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(le‘𝐾) =
(le‘𝐾) |
2 | | eqid 2738 |
. . . 4
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
3 | | trlcnv.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 1, 2, 3 | lhpexnle 37640 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ (Atoms‘𝐾) ¬ 𝑝(le‘𝐾)𝑊) |
5 | 4 | adantr 484 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ∃𝑝 ∈ (Atoms‘𝐾) ¬ 𝑝(le‘𝐾)𝑊) |
6 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) |
7 | | trlcnv.t |
. . . . . . . . . 10
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
8 | 6, 3, 7 | ltrn1o 37758 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) |
9 | 8 | 3adant3 1133 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) |
10 | | simp3l 1202 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝑝 ∈ (Atoms‘𝐾)) |
11 | 6, 2 | atbase 36923 |
. . . . . . . . 9
⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ (Base‘𝐾)) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝑝 ∈ (Base‘𝐾)) |
13 | | f1ocnvfv1 7045 |
. . . . . . . 8
⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾)) → (◡𝐹‘(𝐹‘𝑝)) = 𝑝) |
14 | 9, 12, 13 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (◡𝐹‘(𝐹‘𝑝)) = 𝑝) |
15 | 14 | oveq2d 7187 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝))) = ((𝐹‘𝑝)(join‘𝐾)𝑝)) |
16 | | simp1l 1198 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝐾 ∈ HL) |
17 | 1, 2, 3, 7 | ltrnat 37774 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑝 ∈ (Atoms‘𝐾)) → (𝐹‘𝑝) ∈ (Atoms‘𝐾)) |
18 | 17 | 3adant3r 1182 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝐹‘𝑝) ∈ (Atoms‘𝐾)) |
19 | | eqid 2738 |
. . . . . . . 8
⊢
(join‘𝐾) =
(join‘𝐾) |
20 | 19, 2 | hlatjcom 37002 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(𝐹‘𝑝))) |
21 | 16, 18, 10, 20 | syl3anc 1372 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(𝐹‘𝑝))) |
22 | 15, 21 | eqtrd 2773 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝))) = (𝑝(join‘𝐾)(𝐹‘𝑝))) |
23 | 22 | oveq1d 7186 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝)))(meet‘𝐾)𝑊) = ((𝑝(join‘𝐾)(𝐹‘𝑝))(meet‘𝐾)𝑊)) |
24 | | simp1 1137 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
25 | 3, 7 | ltrncnv 37780 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇) |
26 | 25 | 3adant3 1133 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ◡𝐹 ∈ 𝑇) |
27 | 1, 2, 3, 7 | ltrnel 37773 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (𝐹‘𝑝)(le‘𝐾)𝑊)) |
28 | | eqid 2738 |
. . . . . 6
⊢
(meet‘𝐾) =
(meet‘𝐾) |
29 | | trlcnv.r |
. . . . . 6
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
30 | 1, 19, 28, 2, 3, 7,
29 | trlval2 37797 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ◡𝐹 ∈ 𝑇 ∧ ((𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (𝐹‘𝑝)(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝)))(meet‘𝐾)𝑊)) |
31 | 24, 26, 27, 30 | syl3anc 1372 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝)))(meet‘𝐾)𝑊)) |
32 | 1, 19, 28, 2, 3, 7,
29 | trlval2 37797 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘𝐹) = ((𝑝(join‘𝐾)(𝐹‘𝑝))(meet‘𝐾)𝑊)) |
33 | 23, 31, 32 | 3eqtr4d 2783 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (𝑅‘𝐹)) |
34 | 33 | 3expa 1119 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (𝑅‘𝐹)) |
35 | 5, 34 | rexlimddv 3201 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘◡𝐹) = (𝑅‘𝐹)) |