Metamath Proof Explorer

Theorem 2atm2atN

Description: Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2atm2at.j 
|- .\/ = ( join ` K )
2atm2at.m 
|- ./\ = ( meet ` K )
2atm2at.z 
|- .0. = ( 0. ` K )
2atm2at.a 
|- A = ( Atoms ` K )
Assertion 2atm2atN 
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( R .\/ P ) ./\ ( R .\/ Q ) ) =/= .0. )

Proof

Step Hyp Ref Expression
1 2atm2at.j 
 |-  .\/ = ( join ` K )
2 2atm2at.m 
 |-  ./\ = ( meet ` K )
3 2atm2at.z 
 |-  .0. = ( 0. ` K )
4 2atm2at.a 
 |-  A = ( Atoms ` K )
5 hlop 
 |-  ( K e. HL -> K e. OP )
6 5 adantr 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> K e. OP )
7 simpr3 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R e. A )
8 eqid 
 |-  ( lt ` K ) = ( lt ` K )
9 3 8 4 0ltat 
 |-  ( ( K e. OP /\ R e. A ) -> .0. ( lt ` K ) R )
10 6 7 9 syl2anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> .0. ( lt ` K ) R )
11 simpl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> K e. HL )
12 simpr1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> P e. A )
13 eqid 
 |-  ( le ` K ) = ( le ` K )
14 13 1 4 hlatlej1 
 |-  ( ( K e. HL /\ R e. A /\ P e. A ) -> R ( le ` K ) ( R .\/ P ) )
15 11 7 12 14 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R ( le ` K ) ( R .\/ P ) )
16 simpr2 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> Q e. A )
17 13 1 4 hlatlej1 
 |-  ( ( K e. HL /\ R e. A /\ Q e. A ) -> R ( le ` K ) ( R .\/ Q ) )
18 11 7 16 17 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R ( le ` K ) ( R .\/ Q ) )
19 hllat 
 |-  ( K e. HL -> K e. Lat )
20 19 adantr 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> K e. Lat )
21 eqid 
 |-  ( Base ` K ) = ( Base ` K )
22 21 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
23 7 22 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R e. ( Base ` K ) )
24 21 1 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ P e. A ) -> ( R .\/ P ) e. ( Base ` K ) )
25 11 7 12 24 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( R .\/ P ) e. ( Base ` K ) )
26 21 1 4 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ Q e. A ) -> ( R .\/ Q ) e. ( Base ` K ) )
27 11 7 16 26 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( R .\/ Q ) e. ( Base ` K ) )
28 21 13 2 latlem12 
 |-  ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ ( R .\/ P ) e. ( Base ` K ) /\ ( R .\/ Q ) e. ( Base ` K ) ) ) -> ( ( R ( le ` K ) ( R .\/ P ) /\ R ( le ` K ) ( R .\/ Q ) ) <-> R ( le ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) ) )
29 20 23 25 27 28 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( R ( le ` K ) ( R .\/ P ) /\ R ( le ` K ) ( R .\/ Q ) ) <-> R ( le ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) ) )
30 15 18 29 mpbi2and 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R ( le ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) )
31 hlpos 
 |-  ( K e. HL -> K e. Poset )
32 31 adantr 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> K e. Poset )
33 21 3 op0cl 
 |-  ( K e. OP -> .0. e. ( Base ` K ) )
34 6 33 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> .0. e. ( Base ` K ) )
35 21 2 latmcl 
 |-  ( ( K e. Lat /\ ( R .\/ P ) e. ( Base ` K ) /\ ( R .\/ Q ) e. ( Base ` K ) ) -> ( ( R .\/ P ) ./\ ( R .\/ Q ) ) e. ( Base ` K ) )
36 20 25 27 35 syl3anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( R .\/ P ) ./\ ( R .\/ Q ) ) e. ( Base ` K ) )
37 21 13 8 pltletr 
 |-  ( ( K e. Poset /\ ( .0. e. ( Base ` K ) /\ R e. ( Base ` K ) /\ ( ( R .\/ P ) ./\ ( R .\/ Q ) ) e. ( Base ` K ) ) ) -> ( ( .0. ( lt ` K ) R /\ R ( le ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) ) -> .0. ( lt ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) ) )
38 32 34 23 36 37 syl13anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( .0. ( lt ` K ) R /\ R ( le ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) ) -> .0. ( lt ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) ) )
39 10 30 38 mp2and 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> .0. ( lt ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) )
40 21 8 3 opltn0 
 |-  ( ( K e. OP /\ ( ( R .\/ P ) ./\ ( R .\/ Q ) ) e. ( Base ` K ) ) -> ( .0. ( lt ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) <-> ( ( R .\/ P ) ./\ ( R .\/ Q ) ) =/= .0. ) )
41 6 36 40 syl2anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( .0. ( lt ` K ) ( ( R .\/ P ) ./\ ( R .\/ Q ) ) <-> ( ( R .\/ P ) ./\ ( R .\/ Q ) ) =/= .0. ) )
42 39 41 mpbid 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( R .\/ P ) ./\ ( R .\/ Q ) ) =/= .0. )