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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlatlej.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	hlatlej.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlatlej.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		hlatlej.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		hlatlej.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4	1 2 3	hlatlej1	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge P\in A\right)\to Q\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }P\right)$$
5	4	3com23	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to Q\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }P\right)$$
6	2 3	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }P$$
7	5 6	breqtrrd	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to Q\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$