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 = ( _|_P ` K )
Assertion pnonsingN
|- ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) = (/) )

Proof

Step Hyp Ref Expression
1 2polat.a
 |-  A = ( Atoms ` K )
2 2polat.p
 |-  P = ( _|_P ` K )
3 1 2 2polssN
 |-  ( ( K e. HL /\ X C_ A ) -> X C_ ( P ` ( P ` X ) ) )
4 3 ssrind
 |-  ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) C_ ( ( P ` ( P ` X ) ) i^i ( P ` X ) ) )
5 eqid
 |-  ( lub ` K ) = ( lub ` K )
6 eqid
 |-  ( pmap ` K ) = ( pmap ` K )
7 5 1 6 2 2polvalN
 |-  ( ( K e. HL /\ X C_ A ) -> ( P ` ( P ` X ) ) = ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) )
8 eqid
 |-  ( oc ` K ) = ( oc ` K )
9 5 8 1 6 2 polval2N
 |-  ( ( K e. HL /\ X C_ A ) -> ( P ` X ) = ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) )
10 7 9 ineq12d
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( P ` ( P ` X ) ) i^i ( P ` X ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) )
11 hlop
 |-  ( K e. HL -> K e. OP )
12 11 adantr
 |-  ( ( K e. HL /\ X C_ A ) -> K e. OP )
13 hlclat
 |-  ( K e. HL -> K e. CLat )
14 eqid
 |-  ( Base ` K ) = ( Base ` K )
15 14 1 atssbase
 |-  A C_ ( Base ` K )
16 sstr
 |-  ( ( X C_ A /\ A C_ ( Base ` K ) ) -> X C_ ( Base ` K ) )
17 15 16 mpan2
 |-  ( X C_ A -> X C_ ( Base ` K ) )
18 14 5 clatlubcl
 |-  ( ( K e. CLat /\ X C_ ( Base ` K ) ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
19 13 17 18 syl2an
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( lub ` K ) ` X ) e. ( Base ` K ) )
20 eqid
 |-  ( meet ` K ) = ( meet ` K )
21 eqid
 |-  ( 0. ` K ) = ( 0. ` K )
22 14 8 20 21 opnoncon
 |-  ( ( K e. OP /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) = ( 0. ` K ) )
23 12 19 22 syl2anc
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) = ( 0. ` K ) )
24 23 fveq2d
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = ( ( pmap ` K ) ` ( 0. ` K ) ) )
25 simpl
 |-  ( ( K e. HL /\ X C_ A ) -> K e. HL )
26 14 8 opoccl
 |-  ( ( K e. OP /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) )
27 12 19 26 syl2anc
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) )
28 14 20 1 6 pmapmeet
 |-  ( ( K e. HL /\ ( ( lub ` K ) ` X ) e. ( Base ` K ) /\ ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) e. ( Base ` K ) ) -> ( ( pmap ` K ) ` ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) )
29 25 19 27 28 syl3anc
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( ( ( lub ` K ) ` X ) ( meet ` K ) ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) )
30 hlatl
 |-  ( K e. HL -> K e. AtLat )
31 30 adantr
 |-  ( ( K e. HL /\ X C_ A ) -> K e. AtLat )
32 21 6 pmap0
 |-  ( K e. AtLat -> ( ( pmap ` K ) ` ( 0. ` K ) ) = (/) )
33 31 32 syl
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( pmap ` K ) ` ( 0. ` K ) ) = (/) )
34 24 29 33 3eqtr3d
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( ( pmap ` K ) ` ( ( lub ` K ) ` X ) ) i^i ( ( pmap ` K ) ` ( ( oc ` K ) ` ( ( lub ` K ) ` X ) ) ) ) = (/) )
35 10 34 eqtrd
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( P ` ( P ` X ) ) i^i ( P ` X ) ) = (/) )
36 4 35 sseqtrd
 |-  ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) C_ (/) )
37 ss0b
 |-  ( ( X i^i ( P ` X ) ) C_ (/) <-> ( X i^i ( P ` X ) ) = (/) )
38 36 37 sylib
 |-  ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) = (/) )