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 𝐴 = ( Atoms ‘ 𝐾 )
2polat.p 𝑃 = ( ⊥𝑃𝐾 )
Assertion pnonsingN ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( 𝑋 ∩ ( 𝑃𝑋 ) ) = ∅ )

Proof

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