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