This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) = (/) )