Metamath Proof Explorer

Theorem atnlej1

Description: If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012)

Ref Expression
Hypotheses atnlej.l 
|- .<_ = ( le ` K )
atnlej.j 
|- .\/ = ( join ` K )
atnlej.a 
|- A = ( Atoms ` K )
Assertion atnlej1 
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> P =/= Q )

Proof

Step Hyp Ref Expression
1 atnlej.l 
 |-  .<_ = ( le ` K )
2 atnlej.j 
 |-  .\/ = ( join ` K )
3 atnlej.a 
 |-  A = ( Atoms ` K )
4 hllat 
 |-  ( K e. HL -> K e. Lat )
5 4 3ad2ant1 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> K e. Lat )
6 simp21 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> P e. A )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
9 6 8 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> P e. ( Base ` K ) )
10 simp22 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> Q e. A )
11 7 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
12 10 11 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> Q e. ( Base ` K ) )
13 simp23 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> R e. A )
14 7 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
15 13 14 syl 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> R e. ( Base ` K ) )
16 simp3 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> -. P .<_ ( Q .\/ R ) )
17 7 1 2 latnlej1l 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) /\ -. P .<_ ( Q .\/ R ) ) -> P =/= Q )
18 5 9 12 15 16 17 syl131anc 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> P =/= Q )