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

Metamath Proof Explorer

Theorem 4atlem12

Description: Lemma for 4at . Combine all four possible cases. (Contributed by NM, 11-Jul-2012)

Ref Expression
Hypotheses 4at.l 
|- .<_ = ( le ` K )
4at.j 
|- .\/ = ( join ` K )
4at.a 
|- A = ( Atoms ` K )
Assertion 4atlem12 
|- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )

Proof

Step Hyp Ref Expression
1 4at.l 
 |-  .<_ = ( le ` K )
2 4at.j 
 |-  .\/ = ( join ` K )
3 4at.a 
 |-  A = ( Atoms ` K )
4 simpl11 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. HL )
5 4 hllatd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. Lat )
6 simpl12 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P e. A )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 3 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
9 6 8 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P e. ( Base ` K ) )
10 simpl13 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. A )
11 7 3 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
12 10 11 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. ( Base ` K ) )
13 simpl23 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> T e. A )
14 simpl31 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> U e. A )
15 7 2 3 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
16 4 13 14 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( T .\/ U ) e. ( Base ` K ) )
17 simpl32 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> V e. A )
18 simpl33 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> W e. A )
19 7 2 3 hlatjcl 
 |-  ( ( K e. HL /\ V e. A /\ W e. A ) -> ( V .\/ W ) e. ( Base ` K ) )
20 4 17 18 19 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( V .\/ W ) e. ( Base ` K ) )
21 7 2 latjcl 
 |-  ( ( K e. Lat /\ ( T .\/ U ) e. ( Base ` K ) /\ ( V .\/ W ) e. ( Base ` K ) ) -> ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
22 5 16 20 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) )
23 7 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( P .\/ Q ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
24 5 9 12 22 23 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( P .\/ Q ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
25 simpl21 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. A )
26 7 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
27 25 26 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. ( Base ` K ) )
28 simpl22 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. A )
29 7 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
30 28 29 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. ( Base ` K ) )
31 7 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( R e. ( Base ` K ) /\ S e. ( Base ` K ) /\ ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
32 5 27 30 22 31 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
33 24 32 anbi12d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) <-> ( ( P .\/ Q ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
34 simpl1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
35 7 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
36 34 35 syl 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
37 7 2 3 hlatjcl 
 |-  ( ( K e. HL /\ R e. A /\ S e. A ) -> ( R .\/ S ) e. ( Base ` K ) )
38 4 25 28 37 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R .\/ S ) e. ( Base ` K ) )
39 7 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) e. ( Base ` K ) /\ ( R .\/ S ) e. ( Base ` K ) /\ ( ( T .\/ U ) .\/ ( V .\/ W ) ) e. ( Base ` K ) ) ) -> ( ( ( P .\/ Q ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
40 5 36 38 22 39 syl13anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ ( R .\/ S ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) <-> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
41 33 40 bitrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) <-> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
42 simp1l 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
43 simp1r 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
44 simp2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> -. P .<_ ( ( U .\/ V ) .\/ W ) )
45 simp3 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
46 1 2 3 4atlem12b 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
47 42 43 44 45 46 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. P .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
48 47 3exp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. P .<_ ( ( U .\/ V ) .\/ W ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
49 7 2 latj4rot 
 |-  ( ( K e. Lat /\ ( Q e. ( Base ` K ) /\ R e. ( Base ` K ) ) /\ ( S e. ( Base ` K ) /\ P e. ( Base ` K ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ P ) ) = ( ( P .\/ Q ) .\/ ( R .\/ S ) ) )
50 5 12 27 30 9 49 syl122anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ P ) ) = ( ( P .\/ Q ) .\/ ( R .\/ S ) ) )
51 50 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ P ) ) = ( ( P .\/ Q ) .\/ ( R .\/ S ) ) )
52 4 10 25 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( K e. HL /\ Q e. A /\ R e. A ) )
53 28 6 13 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S e. A /\ P e. A /\ T e. A ) )
54 simpl3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( U e. A /\ V e. A /\ W e. A ) )
55 52 53 54 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( S e. A /\ P e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
56 55 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( S e. A /\ P e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
57 simpr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
58 1 2 3 4noncolr3 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. P .<_ ( ( Q .\/ R ) .\/ S ) ) )
59 34 25 28 57 58 syl121anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. P .<_ ( ( Q .\/ R ) .\/ S ) ) )
60 59 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. P .<_ ( ( Q .\/ R ) .\/ S ) ) )
61 simp2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> -. Q .<_ ( ( U .\/ V ) .\/ W ) )
62 simprlr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
63 simprrl 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
64 62 63 jca 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
65 simprrr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
66 simprll 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
67 64 65 66 jca32 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
68 67 3adant2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
69 1 2 3 4atlem12b 
 |-  ( ( ( ( K e. HL /\ Q e. A /\ R e. A ) /\ ( S e. A /\ P e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( Q =/= R /\ -. S .<_ ( Q .\/ R ) /\ -. P .<_ ( ( Q .\/ R ) .\/ S ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ P ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
70 56 60 61 68 69 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( Q .\/ R ) .\/ ( S .\/ P ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
71 51 70 eqtr3d 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. Q .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
72 71 3exp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. Q .<_ ( ( U .\/ V ) .\/ W ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
73 48 72 jaod 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( -. P .<_ ( ( U .\/ V ) .\/ W ) \/ -. Q .<_ ( ( U .\/ V ) .\/ W ) ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
74 7 2 latjcom 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ ( R .\/ S ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( R .\/ S ) .\/ ( P .\/ Q ) ) )
75 5 36 38 74 syl3anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( R .\/ S ) .\/ ( P .\/ Q ) ) )
76 75 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( R .\/ S ) .\/ ( P .\/ Q ) ) )
77 4 25 28 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( K e. HL /\ R e. A /\ S e. A ) )
78 6 10 13 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P e. A /\ Q e. A /\ T e. A ) )
79 77 78 54 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( K e. HL /\ R e. A /\ S e. A ) /\ ( P e. A /\ Q e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
80 79 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( K e. HL /\ R e. A /\ S e. A ) /\ ( P e. A /\ Q e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
81 1 2 3 4noncolr2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R =/= S /\ -. P .<_ ( R .\/ S ) /\ -. Q .<_ ( ( R .\/ S ) .\/ P ) ) )
82 34 25 28 57 81 syl121anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R =/= S /\ -. P .<_ ( R .\/ S ) /\ -. Q .<_ ( ( R .\/ S ) .\/ P ) ) )
83 82 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( R =/= S /\ -. P .<_ ( R .\/ S ) /\ -. Q .<_ ( ( R .\/ S ) .\/ P ) ) )
84 simp2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> -. R .<_ ( ( U .\/ V ) .\/ W ) )
85 simprr 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
86 simprl 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
87 85 86 jca 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
88 87 3adant2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
89 1 2 3 4atlem12b 
 |-  ( ( ( ( K e. HL /\ R e. A /\ S e. A ) /\ ( P e. A /\ Q e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( R =/= S /\ -. P .<_ ( R .\/ S ) /\ -. Q .<_ ( ( R .\/ S ) .\/ P ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( R .\/ S ) .\/ ( P .\/ Q ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
90 80 83 84 88 89 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( R .\/ S ) .\/ ( P .\/ Q ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
91 76 90 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. R .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
92 91 3exp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. R .<_ ( ( U .\/ V ) .\/ W ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
93 7 2 latj4rot 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) /\ ( R e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( S .\/ P ) .\/ ( Q .\/ R ) ) )
94 5 9 12 27 30 93 syl122anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( S .\/ P ) .\/ ( Q .\/ R ) ) )
95 94 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( S .\/ P ) .\/ ( Q .\/ R ) ) )
96 4 28 6 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( K e. HL /\ S e. A /\ P e. A ) )
97 10 25 13 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( Q e. A /\ R e. A /\ T e. A ) )
98 96 97 54 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( K e. HL /\ S e. A /\ P e. A ) /\ ( Q e. A /\ R e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
99 98 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( K e. HL /\ S e. A /\ P e. A ) /\ ( Q e. A /\ R e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) )
100 1 2 3 4noncolr1 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S =/= P /\ -. Q .<_ ( S .\/ P ) /\ -. R .<_ ( ( S .\/ P ) .\/ Q ) ) )
101 34 25 28 57 100 syl121anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S =/= P /\ -. Q .<_ ( S .\/ P ) /\ -. R .<_ ( ( S .\/ P ) .\/ Q ) ) )
102 101 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( S =/= P /\ -. Q .<_ ( S .\/ P ) /\ -. R .<_ ( ( S .\/ P ) .\/ Q ) ) )
103 simp2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> -. S .<_ ( ( U .\/ V ) .\/ W ) )
104 65 66 jca 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
105 104 62 63 jca32 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
106 105 3adant2 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
107 1 2 3 4atlem12b 
 |-  ( ( ( ( K e. HL /\ S e. A /\ P e. A ) /\ ( Q e. A /\ R e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( ( S =/= P /\ -. Q .<_ ( S .\/ P ) /\ -. R .<_ ( ( S .\/ P ) .\/ Q ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) ) /\ ( ( S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( S .\/ P ) .\/ ( Q .\/ R ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
108 99 102 103 106 107 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( S .\/ P ) .\/ ( Q .\/ R ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
109 95 108 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) /\ -. S .<_ ( ( U .\/ V ) .\/ W ) /\ ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) )
110 109 3exp 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( -. S .<_ ( ( U .\/ V ) .\/ W ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
111 92 110 jaod 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( -. R .<_ ( ( U .\/ V ) .\/ W ) \/ -. S .<_ ( ( U .\/ V ) .\/ W ) ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) )
112 25 28 14 3jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R e. A /\ S e. A /\ U e. A ) )
113 17 18 jca 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( V e. A /\ W e. A ) )
114 1 2 3 4atlem3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ U e. A ) /\ ( V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( -. P .<_ ( ( U .\/ V ) .\/ W ) \/ -. Q .<_ ( ( U .\/ V ) .\/ W ) ) \/ ( -. R .<_ ( ( U .\/ V ) .\/ W ) \/ -. S .<_ ( ( U .\/ V ) .\/ W ) ) ) )
115 34 112 113 57 114 syl31anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( -. P .<_ ( ( U .\/ V ) .\/ W ) \/ -. Q .<_ ( ( U .\/ V ) .\/ W ) ) \/ ( -. R .<_ ( ( U .\/ V ) .\/ W ) \/ -. S .<_ ( ( U .\/ V ) .\/ W ) ) ) )
116 73 111 115 mpjaod 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ Q .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) /\ ( R .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) /\ S .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )
117 41 116 sylbird 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ T e. A ) /\ ( U e. A /\ V e. A /\ W e. A ) ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ ( R .\/ S ) ) .<_ ( ( T .\/ U ) .\/ ( V .\/ W ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( T .\/ U ) .\/ ( V .\/ W ) ) ) )