Theorem hlatlej2

Description: A join's second argument is less than or equal to the join. Special case of latlej2 to show an atom is on a line. (Contributed by NM, 15-May-2013)

	Ref	Expression
Hypotheses	hlatlej.l	⊢ ≤ = ( le ‘ 𝐾 )
	hlatlej.j	⊢ ∨ = ( join ‘ 𝐾 )
	hlatlej.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlatlej2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		hlatlej.l	⊢ ≤ = ( le ‘ 𝐾 )
2		hlatlej.j	⊢ ∨ = ( join ‘ 𝐾 )
3		hlatlej.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4	1 2 3	hlatlej1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑄 ∨ 𝑃 ) )
5	4	3com23	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑄 ∨ 𝑃 ) )
6	2 3	hlatjcom	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
7	5 6	breqtrrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑄 ) )