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 ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) = ∅) |