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 =