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 ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≠ 𝑅 )