Proof of Theorem pnonsingN
| Step | Hyp | Ref
| Expression |
| 1 | | 2polat.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
| 2 | | 2polat.p |
. . . . 5
⊢ 𝑃 =
(⊥𝑃‘𝐾) |
| 3 | 1, 2 | 2polssN 39917 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ (𝑃‘(𝑃‘𝑋))) |
| 4 | 3 | ssrind 4244 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) ⊆ ((𝑃‘(𝑃‘𝑋)) ∩ (𝑃‘𝑋))) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(lub‘𝐾) =
(lub‘𝐾) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(pmap‘𝐾) =
(pmap‘𝐾) |
| 7 | 5, 1, 6, 2 | 2polvalN 39916 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑃‘(𝑃‘𝑋)) = ((pmap‘𝐾)‘((lub‘𝐾)‘𝑋))) |
| 8 | | eqid 2737 |
. . . . . 6
⊢
(oc‘𝐾) =
(oc‘𝐾) |
| 9 | 5, 8, 1, 6, 2 | polval2N 39908 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) |
| 10 | 7, 9 | ineq12d 4221 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((𝑃‘(𝑃‘𝑋)) ∩ (𝑃‘𝑋)) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))) |
| 11 | | hlop 39363 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
| 12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ OP) |
| 13 | | hlclat 39359 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
| 14 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 15 | 14, 1 | atssbase 39291 |
. . . . . . . . 9
⊢ 𝐴 ⊆ (Base‘𝐾) |
| 16 | | sstr 3992 |
. . . . . . . . 9
⊢ ((𝑋 ⊆ 𝐴 ∧ 𝐴 ⊆ (Base‘𝐾)) → 𝑋 ⊆ (Base‘𝐾)) |
| 17 | 15, 16 | mpan2 691 |
. . . . . . . 8
⊢ (𝑋 ⊆ 𝐴 → 𝑋 ⊆ (Base‘𝐾)) |
| 18 | 14, 5 | clatlubcl 18548 |
. . . . . . . 8
⊢ ((𝐾 ∈ CLat ∧ 𝑋 ⊆ (Base‘𝐾)) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
| 19 | 13, 17, 18 | syl2an 596 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
| 20 | | eqid 2737 |
. . . . . . . 8
⊢
(meet‘𝐾) =
(meet‘𝐾) |
| 21 | | eqid 2737 |
. . . . . . . 8
⊢
(0.‘𝐾) =
(0.‘𝐾) |
| 22 | 14, 8, 20, 21 | opnoncon 39209 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → (((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) = (0.‘𝐾)) |
| 23 | 12, 19, 22 | syl2anc 584 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋))) = (0.‘𝐾)) |
| 24 | 23 | fveq2d 6910 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = ((pmap‘𝐾)‘(0.‘𝐾))) |
| 25 | | simpl 482 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ HL) |
| 26 | 14, 8 | opoccl 39195 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) |
| 27 | 12, 19, 26 | syl2anc 584 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) |
| 28 | 14, 20, 1, 6 | pmapmeet 39775 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧
((lub‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘((lub‘𝐾)‘𝑋)) ∈ (Base‘𝐾)) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))) |
| 29 | 25, 19, 27, 28 | syl3anc 1373 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘(((lub‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋))))) |
| 30 | | hlatl 39361 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
| 31 | 30 | adantr 480 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ AtLat) |
| 32 | 21, 6 | pmap0 39767 |
. . . . . 6
⊢ (𝐾 ∈ AtLat →
((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
| 33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((pmap‘𝐾)‘(0.‘𝐾)) = ∅) |
| 34 | 24, 29, 33 | 3eqtr3d 2785 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (((pmap‘𝐾)‘((lub‘𝐾)‘𝑋)) ∩ ((pmap‘𝐾)‘((oc‘𝐾)‘((lub‘𝐾)‘𝑋)))) = ∅) |
| 35 | 10, 34 | eqtrd 2777 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ((𝑃‘(𝑃‘𝑋)) ∩ (𝑃‘𝑋)) = ∅) |
| 36 | 4, 35 | sseqtrd 4020 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) ⊆ ∅) |
| 37 | | ss0b 4401 |
. 2
⊢ ((𝑋 ∩ (𝑃‘𝑋)) ⊆ ∅ ↔ (𝑋 ∩ (𝑃‘𝑋)) = ∅) |
| 38 | 36, 37 | sylib 218 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) = ∅) |