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 )