Metamath Proof Explorer

Theorem pnonsingN

Description: The intersection of a set of atoms and its polarity is empty. Definition of nonsingular in Holland95 p. 214. (Contributed by NM, 29-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2polat.a ⊢ A = Atoms ⁡ K
2polat.p ⊢ P = ⊥ 𝑃 ⁡ K
Assertion pnonsingN ⊢ K ∈ HL ∧ X ⊆ A → X ∩ P ⁡ X = ∅

Proof

Step Hyp Ref Expression
1 2polat.a ⊢ A = Atoms ⁡ K
2 2polat.p ⊢ P = ⊥ 𝑃 ⁡ K
3 1 2 2polssN ⊢ K ∈ HL ∧ X ⊆ A → X ⊆ P ⁡ P ⁡ X
4 3 ssrind ⊢ K ∈ HL ∧ X ⊆ A → X ∩ P ⁡ X ⊆ P ⁡ P ⁡ X ∩ P ⁡ X
5 eqid ⊢ lub ⁡ K = lub ⁡ K
6 eqid ⊢ pmap ⁡ K = pmap ⁡ K
7 5 1 6 2 2polvalN ⊢ K ∈ HL ∧ X ⊆ A → P ⁡ P ⁡ X = pmap ⁡ K ⁡ lub ⁡ K ⁡ X
8 eqid ⊢ oc ⁡ K = oc ⁡ K
9 5 8 1 6 2 polval2N ⊢ K ∈ HL ∧ X ⊆ A → P ⁡ X = pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X
10 7 9 ineq12d ⊢ K ∈ HL ∧ X ⊆ A → P ⁡ P ⁡ X ∩ P ⁡ X = pmap ⁡ K ⁡ lub ⁡ K ⁡ X ∩ pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X
11 hlop ⊢ K ∈ HL → K ∈ OP
12 11 adantr ⊢ K ∈ HL ∧ X ⊆ A → K ∈ OP
13 hlclat ⊢ K ∈ HL → K ∈ CLat
14 eqid ⊢ Base K = Base K
15 14 1 atssbase ⊢ A ⊆ Base K
16 sstr ⊢ X ⊆ A ∧ A ⊆ Base K → X ⊆ Base K
17 15 16 mpan2 ⊢ X ⊆ A → X ⊆ Base K
18 14 5 clatlubcl ⊢ K ∈ CLat ∧ X ⊆ Base K → lub ⁡ K ⁡ X ∈ Base K
19 13 17 18 syl2an ⊢ K ∈ HL ∧ X ⊆ A → lub ⁡ K ⁡ X ∈ Base K
20 eqid ⊢ meet ⁡ K = meet ⁡ K
21 eqid ⊢ 0. ⁡ K = 0. ⁡ K
22 14 8 20 21 opnoncon ⊢ K ∈ OP ∧ lub ⁡ K ⁡ X ∈ Base K → lub ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ lub ⁡ K ⁡ X = 0. ⁡ K
23 12 19 22 syl2anc ⊢ K ∈ HL ∧ X ⊆ A → lub ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ lub ⁡ K ⁡ X = 0. ⁡ K
24 23 fveq2d ⊢ K ∈ HL ∧ X ⊆ A → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ lub ⁡ K ⁡ X = pmap ⁡ K ⁡ 0. ⁡ K
25 simpl ⊢ K ∈ HL ∧ X ⊆ A → K ∈ HL
26 14 8 opoccl ⊢ K ∈ OP ∧ lub ⁡ K ⁡ X ∈ Base K → oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K
27 12 19 26 syl2anc ⊢ K ∈ HL ∧ X ⊆ A → oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K
28 14 20 1 6 pmapmeet ⊢ K ∈ HL ∧ lub ⁡ K ⁡ X ∈ Base K ∧ oc ⁡ K ⁡ lub ⁡ K ⁡ X ∈ Base K → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ lub ⁡ K ⁡ X = pmap ⁡ K ⁡ lub ⁡ K ⁡ X ∩ pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X
29 25 19 27 28 syl3anc ⊢ K ∈ HL ∧ X ⊆ A → pmap ⁡ K ⁡ lub ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ lub ⁡ K ⁡ X = pmap ⁡ K ⁡ lub ⁡ K ⁡ X ∩ pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X
30 hlatl ⊢ K ∈ HL → K ∈ AtLat
31 30 adantr ⊢ K ∈ HL ∧ X ⊆ A → K ∈ AtLat
32 21 6 pmap0 ⊢ K ∈ AtLat → pmap ⁡ K ⁡ 0. ⁡ K = ∅
33 31 32 syl ⊢ K ∈ HL ∧ X ⊆ A → pmap ⁡ K ⁡ 0. ⁡ K = ∅
34 24 29 33 3eqtr3d ⊢ K ∈ HL ∧ X ⊆ A → pmap ⁡ K ⁡ lub ⁡ K ⁡ X ∩ pmap ⁡ K ⁡ oc ⁡ K ⁡ lub ⁡ K ⁡ X = ∅
35 10 34 eqtrd ⊢ K ∈ HL ∧ X ⊆ A → P ⁡ P ⁡ X ∩ P ⁡ X = ∅
36 4 35 sseqtrd ⊢ K ∈ HL ∧ X ⊆ A → X ∩ P ⁡ X ⊆ ∅
37 ss0b ⊢ X ∩ P ⁡ X ⊆ ∅ ↔ X ∩ P ⁡ X = ∅
38 36 37 sylib ⊢ K ∈ HL ∧ X ⊆ A → X ∩ P ⁡ X = ∅