Theorem hlatlej1

Description: A join's first argument is less than or equal to the join. Special case of latlej1 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	hlatlej1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		hlatlej.l	⊢ ≤ = ( le ‘ 𝐾 )
2		hlatlej.j	⊢ ∨ = ( join ‘ 𝐾 )
3		hlatlej.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6	5 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
7	5 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
8	5 1 2	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )
9	4 6 7 8	syl3an	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )