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

Metamath Proof Explorer

Theorem atnlej2

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 ‘ 𝐾 )
atnlej.j ⊢ ∨ = ( join ‘ 𝐾 )
atnlej.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atnlej2 ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≠ 𝑅 )

Proof

Step Hyp Ref Expression
1 atnlej.l ⊢ ≤ = ( le ‘ 𝐾 )
2 atnlej.j ⊢ ∨ = ( join ‘ 𝐾 )
3 atnlej.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
5 4 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ Lat )
6 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9 6 8 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
11 7 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
14 7 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
16 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
17 7 1 2 latnlej1r ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≠ 𝑅 )
18 5 9 12 15 16 17 syl131anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≠ 𝑅 )