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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlatlej.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	hlatlej.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlatlej1	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\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		hllat	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Lat}$$
5		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
6	5 3	atbase	$$⊢P\in A\to P\in {\mathrm{Base}}_K$$
7	5 3	atbase	$$⊢Q\in A\to Q\in {\mathrm{Base}}_K$$
8	5 1 2	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge P\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\right)\to P\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
9	4 6 7 8	syl3an	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$