Theorem hlatcon3

Description: Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012)

	Ref	Expression
Hypotheses	3noncol.l	⊢ ≤ = ( le ‘ 𝐾 )
	3noncol.j	⊢ ∨ = ( join ‘ 𝐾 )
	3noncol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlatcon3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		3noncol.l	⊢ ≤ = ( le ‘ 𝐾 )
2		3noncol.j	⊢ ∨ = ( join ‘ 𝐾 )
3		3noncol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4	1 2 3	3noncolr2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
5	4	simprd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )