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 ˙ = K
atnlej.j ˙ = join K
atnlej.a A = Atoms K
Assertion atnlej1 K HL P A Q A R A ¬ P ˙ Q ˙ R P Q

Proof

Step Hyp Ref Expression
1 atnlej.l ˙ = K
2 atnlej.j ˙ = join K
3 atnlej.a A = Atoms K
4 hllat K HL K Lat
5 4 3ad2ant1 K HL P A Q A R A ¬ P ˙ Q ˙ R K Lat
6 simp21 K HL P A Q A R A ¬ P ˙ Q ˙ R P A
7 eqid Base K = Base K
8 7 3 atbase P A P Base K
9 6 8 syl K HL P A Q A R A ¬ P ˙ Q ˙ R P Base K
10 simp22 K HL P A Q A R A ¬ P ˙ Q ˙ R Q A
11 7 3 atbase Q A Q Base K
12 10 11 syl K HL P A Q A R A ¬ P ˙ Q ˙ R Q Base K
13 simp23 K HL P A Q A R A ¬ P ˙ Q ˙ R R A
14 7 3 atbase R A R Base K
15 13 14 syl K HL P A Q A R A ¬ P ˙ Q ˙ R R Base K
16 simp3 K HL P A Q A R A ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R
17 7 1 2 latnlej1l K Lat P Base K Q Base K R Base K ¬ P ˙ Q ˙ R P Q
18 5 9 12 15 16 17 syl131anc K HL P A Q A R A ¬ P ˙ Q ˙ R P Q