Proof of Theorem pnonsingN
Step | Hyp | Ref
| Expression |
1 | | 2polat.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
2 | | 2polat.p |
. . . . 5
⊢ 𝑃 =
(⊥𝑃‘𝐾) |
3 | 1, 2 | 2polssN 34219 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ (𝑃‘(𝑃‘𝑋))) |
4 | | ssrin 3800 |
. . . 4
⊢ (𝑋 ⊆ (𝑃‘(𝑃‘𝑋)) → (𝑋 ∩ (𝑃‘𝑋)) ⊆ ((𝑃‘(𝑃‘𝑋)) ∩ (𝑃‘𝑋))) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) ⊆ ((𝑃‘(𝑃‘𝑋)) ∩ (𝑃‘𝑋))) |
6 | | eqid 2610 |
. . . . . 6
⊢
(lub‘𝐾) =
(lub‘𝐾) |
7 | | eqid 2610 |
. . . . . 6
⊢
(pmap‘𝐾) =
(pmap‘𝐾) |
8 | 6, 1, 7, 2 | 2polvalN 34218 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑃‘(𝑃‘𝑋)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋))) |
9 | | eqid 2610 |
. . . . . 6
⊢
(oc‘𝐾) =
(oc‘𝐾) |
10 | 6, 9, 1, 7, 2 | polval2N 34210 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) |
11 | 8, 10 | ineq12d 3777 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((𝑃‘(𝑃‘𝑋)) ∩ (𝑃‘𝑋)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))) |
12 | | hlop 33667 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ OP) |
14 | | hlclat 33663 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
15 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) |
16 | 15, 1 | atssbase 33595 |
. . . . . . . . 9
⊢ 𝐴 ⊆ (Base‘𝐾) |
17 | | sstr 3576 |
. . . . . . . . 9
⊢ ((𝑋 ⊆ 𝐴 ∧ 𝐴 ⊆ (Base‘𝐾)) → 𝑋 ⊆ (Base‘𝐾)) |
18 | 16, 17 | mpan2 703 |
. . . . . . . 8
⊢ (𝑋 ⊆ 𝐴 → 𝑋 ⊆ (Base‘𝐾)) |
19 | 15, 6 | clatlubcl 16935 |
. . . . . . . 8
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
20 | 14, 18, 19 | syl2an 493 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
21 | | eqid 2610 |
. . . . . . . 8
⊢
(meet‘𝐾) =
(meet‘𝐾) |
22 | | eqid 2610 |
. . . . . . . 8
⊢
(0.‘𝐾) =
(0.‘𝐾) |
23 | 15, 9, 21, 22 | opnoncon 33513 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → (((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) = (0.‘𝐾)) |
24 | 13, 20, 23 | syl2anc 691 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) = (0.‘𝐾)) |
25 | 24 | fveq2d 6107 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = ((pmap‘𝐾)‘(0.‘𝐾))) |
26 | | simpl 472 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ HL) |
27 | 15, 9 | opoccl 33499 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) |
28 | 13, 20, 27 | syl2anc 691 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) |
29 | 15, 21, 1, 7 | pmapmeet 34077 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))) |
30 | 26, 20, 28, 29 | syl3anc 1318 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))) |
31 | | hlatl 33665 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ AtLat) |
33 | 22, 7 | pmap0 34069 |
. . . . . 6
⊢ (𝐾 ∈ AtLat →
((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
34 | 32, 33 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
35 | 25, 30, 34 | 3eqtr3d 2652 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = ∅) |
36 | 11, 35 | eqtrd 2644 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((𝑃‘(𝑃‘𝑋)) ∩ (𝑃‘𝑋)) = ∅) |
37 | 5, 36 | sseqtrd 3604 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) ⊆ ∅) |
38 | | ss0b 3925 |
. 2
⊢ ((𝑋 ∩ (𝑃‘𝑋)) ⊆ ∅ ↔ (𝑋 ∩ (𝑃‘𝑋)) = ∅) |
39 | 37, 38 | sylib 207 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) = ∅) |