Theorem atexchltN

Description: Atom exchange property. Version of hlatexch2 with less-than ordering. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atexchlt.s	|- .< = ( lt ` K )
	atexchlt.j	|- .\/ = ( join ` K )
	atexchlt.a	|- A = ( Atoms ` K )
Assertion	atexchltN	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .< ( Q .\/ R ) -> Q .< ( P .\/ R ) ) )

Proof

Step	Hyp	Ref	Expression
1		atexchlt.s	|- .< = ( lt ` K )
2		atexchlt.j	|- .\/ = ( join ` K )
3		atexchlt.a	|- A = ( Atoms ` K )
4		eqid	|- (
5	2 3 4	atexchcvrN	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P ( Q (
6	1 2 3 4	atltcvr	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( P .< ( Q .\/ R ) <-> P (
7	6	3adant3	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .< ( Q .\/ R ) <-> P (
8		simpl	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> K e. HL )
9		simpr2	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> Q e. A )
10		simpr1	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> P e. A )
11		simpr3	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> R e. A )
12	1 2 3 4	atltcvr	|- ( ( K e. HL /\ ( Q e. A /\ P e. A /\ R e. A ) ) -> ( Q .< ( P .\/ R ) <-> Q (
13	8 9 10 11 12	syl13anc	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( Q .< ( P .\/ R ) <-> Q (
14	13	3adant3	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( Q .< ( P .\/ R ) <-> Q (
15	5 7 14	3imtr4d	|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .< ( Q .\/ R ) -> Q .< ( P .\/ R ) ) )