Step | Hyp | Ref
| Expression |
1 | | ssid 3999 |
. . 3
⊢ 𝐴 ⊆ 𝐴 |
2 | | eqid 2725 |
. . . 4
⊢
(lub‘𝐾) =
(lub‘𝐾) |
3 | | eqid 2725 |
. . . 4
⊢
(oc‘𝐾) =
(oc‘𝐾) |
4 | | polssat.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | eqid 2725 |
. . . 4
⊢
(pmap‘𝐾) =
(pmap‘𝐾) |
6 | | polssat.p |
. . . 4
⊢ ⊥ =
(⊥𝑃‘𝐾) |
7 | 2, 3, 4, 5, 6 | polval2N 39506 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝐴 ⊆ 𝐴) → ( ⊥ ‘𝐴) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴)))) |
8 | 1, 7 | mpan2 689 |
. 2
⊢ (𝐾 ∈ HL → ( ⊥
‘𝐴) =
((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴)))) |
9 | | hlop 38961 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
10 | | eqid 2725 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
11 | 10, 4 | atbase 38888 |
. . . . . . . . . 10
⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ (Base‘𝐾)) |
12 | | eqid 2725 |
. . . . . . . . . . 11
⊢
(le‘𝐾) =
(le‘𝐾) |
13 | | eqid 2725 |
. . . . . . . . . . 11
⊢
(1.‘𝐾) =
(1.‘𝐾) |
14 | 10, 12, 13 | ople1 38790 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ OP ∧ 𝑝 ∈ (Base‘𝐾)) → 𝑝(le‘𝐾)(1.‘𝐾)) |
15 | 9, 11, 14 | syl2an 594 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴) → 𝑝(le‘𝐾)(1.‘𝐾)) |
16 | 15 | ralrimiva 3135 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → ∀𝑝 ∈ 𝐴 𝑝(le‘𝐾)(1.‘𝐾)) |
17 | | rabid2 3452 |
. . . . . . . 8
⊢ (𝐴 = {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)} ↔ ∀𝑝 ∈ 𝐴 𝑝(le‘𝐾)(1.‘𝐾)) |
18 | 16, 17 | sylibr 233 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐴 = {𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)}) |
19 | 18 | fveq2d 6900 |
. . . . . 6
⊢ (𝐾 ∈ HL →
((lub‘𝐾)‘𝐴) = ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)})) |
20 | | hlomcmat 38964 |
. . . . . . 7
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat)) |
21 | 10, 13 | op1cl 38784 |
. . . . . . . 8
⊢ (𝐾 ∈ OP →
(1.‘𝐾) ∈
(Base‘𝐾)) |
22 | 9, 21 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ HL →
(1.‘𝐾) ∈
(Base‘𝐾)) |
23 | 10, 12, 2, 4 | atlatmstc 38918 |
. . . . . . 7
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧
(1.‘𝐾) ∈
(Base‘𝐾)) →
((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)}) = (1.‘𝐾)) |
24 | 20, 22, 23 | syl2anc 582 |
. . . . . 6
⊢ (𝐾 ∈ HL →
((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝(le‘𝐾)(1.‘𝐾)}) = (1.‘𝐾)) |
25 | 19, 24 | eqtr2d 2766 |
. . . . 5
⊢ (𝐾 ∈ HL →
(1.‘𝐾) =
((lub‘𝐾)‘𝐴)) |
26 | 25 | fveq2d 6900 |
. . . 4
⊢ (𝐾 ∈ HL →
((oc‘𝐾)‘(1.‘𝐾)) = ((oc‘𝐾)‘((lub‘𝐾)‘𝐴))) |
27 | | eqid 2725 |
. . . . . 6
⊢
(0.‘𝐾) =
(0.‘𝐾) |
28 | 27, 13, 3 | opoc1 38801 |
. . . . 5
⊢ (𝐾 ∈ OP →
((oc‘𝐾)‘(1.‘𝐾)) = (0.‘𝐾)) |
29 | 9, 28 | syl 17 |
. . . 4
⊢ (𝐾 ∈ HL →
((oc‘𝐾)‘(1.‘𝐾)) = (0.‘𝐾)) |
30 | 26, 29 | eqtr3d 2767 |
. . 3
⊢ (𝐾 ∈ HL →
((oc‘𝐾)‘((lub‘𝐾)‘𝐴)) = (0.‘𝐾)) |
31 | 30 | fveq2d 6900 |
. 2
⊢ (𝐾 ∈ HL →
((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝐴))) = ((pmap‘𝐾)‘(0.‘𝐾))) |
32 | | hlatl 38959 |
. . 3
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
33 | 27, 5 | pmap0 39365 |
. . 3
⊢ (𝐾 ∈ AtLat →
((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
34 | 32, 33 | syl 17 |
. 2
⊢ (𝐾 ∈ HL →
((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
35 | 8, 31, 34 | 3eqtrd 2769 |
1
⊢ (𝐾 ∈ HL → ( ⊥
‘𝐴) =
∅) |