This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )