Theorem paddasslem1

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	paddasslem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	paddasslem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	paddasslem1	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(x\in A\wedge r\in A\wedge y\in A\right)\wedge x\ne y\right)\wedge \neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\to \neg x\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)$$

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		paddasslem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		paddasslem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4	1 2 3	hlatexch2	$$⊢\left(K\in \mathrm{HL}\wedge \left(x\in A\wedge r\in A\wedge y\in A\right)\wedge x\ne y\right)\to \left(x\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)\to r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)$$
5	4	con3dimp	$$⊢\left(\left(K\in \mathrm{HL}\wedge \left(x\in A\wedge r\in A\wedge y\in A\right)\wedge x\ne y\right)\wedge \neg r\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\to \neg x\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }y\right)$$