Metamath Proof Explorer

Theorem 2lplnja

Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj in terms of atoms). (Contributed by NM, 12-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 2lplnja.l 
 |-  .<_ = ( le ` K )
2 2lplnja.j 
 |-  .\/ = ( join ` K )
3 2lplnja.a 
 |-  A = ( Atoms ` K )
4 2lplnja.v 
 |-  V = ( LVols ` K )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> K e. HL )
7 6 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> K e. Lat )
8 simp121 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> P e. A )
9 simp122 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> Q e. A )
10 5 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
11 6 8 9 10 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
12 simp123 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> R e. A )
13 5 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
14 12 13 syl 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> R e. ( Base ` K ) )
15 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
16 7 11 14 15 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
17 simp2l1 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> S e. A )
18 simp2l2 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> T e. A )
19 5 2 3 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ T e. A ) -> ( S .\/ T ) e. ( Base ` K ) )
20 6 17 18 19 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( S .\/ T ) e. ( Base ` K ) )
21 simp2l3 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> U e. A )
22 5 3 atbase 
 |-  ( U e. A -> U e. ( Base ` K ) )
23 21 22 syl 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> U e. ( Base ` K ) )
24 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( S .\/ T ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> ( ( S .\/ T ) .\/ U ) e. ( Base ` K ) )
25 7 20 23 24 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( S .\/ T ) .\/ U ) e. ( Base ` K ) )
26 5 2 latjcl 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) /\ ( ( S .\/ T ) .\/ U ) e. ( Base ` K ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) e. ( Base ` K ) )
27 7 16 25 26 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) e. ( Base ` K ) )
28 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> W e. V )
29 5 4 lvolbase 
 |-  ( W e. V -> W e. ( Base ` K ) )
30 28 29 syl 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> W e. ( Base ` K ) )
31 simp31 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( P .\/ Q ) .\/ R ) .<_ W )
32 simp32 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( S .\/ T ) .\/ U ) .<_ W )
33 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) /\ ( ( S .\/ T ) .\/ U ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) .<_ W ) )
34 7 16 25 30 33 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) .<_ W ) )
35 31 32 34 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) .<_ W )
36 5 1 2 latlej2 
 |-  ( ( K e. Lat /\ ( S .\/ T ) e. ( Base ` K ) /\ U e. ( Base ` K ) ) -> U .<_ ( ( S .\/ T ) .\/ U ) )
37 7 20 23 36 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> U .<_ ( ( S .\/ T ) .\/ U ) )
38 5 1 7 23 25 30 37 32 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> U .<_ W )
39 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) /\ U e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ U .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ W ) )
40 7 16 23 30 39 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ U .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ W ) )
41 31 38 40 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ W )
42 41 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ W )
43 6 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> K e. HL )
44 6 8 9 3jca 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
45 44 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
46 12 21 jca 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( R e. A /\ U e. A ) )
47 46 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( R e. A /\ U e. A ) )
48 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> P =/= Q )
49 48 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> P =/= Q )
50 simp13r 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> -. R .<_ ( P .\/ Q ) )
51 50 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> -. R .<_ ( P .\/ Q ) )
52 simp33 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) )
53 52 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) )
54 simplr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> S .<_ ( ( P .\/ Q ) .\/ R ) )
55 simpr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> T .<_ ( ( P .\/ Q ) .\/ R ) )
56 5 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
57 17 56 syl 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> S e. ( Base ` K ) )
58 5 3 atbase 
 |-  ( T e. A -> T e. ( Base ` K ) )
59 18 58 syl 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> T e. ( Base ` K ) )
60 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) ) -> ( ( S .<_ ( ( P .\/ Q ) .\/ R ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) <-> ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) ) )
61 7 57 59 16 60 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( S .<_ ( ( P .\/ Q ) .\/ R ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) <-> ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) ) )
62 61 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( S .<_ ( ( P .\/ Q ) .\/ R ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) <-> ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) ) )
63 54 55 62 mpbi2and 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) )
64 63 adantr 
 |-  ( ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) )
65 simpr 
 |-  ( ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) -> U .<_ ( ( P .\/ Q ) .\/ R ) )
66 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( S .\/ T ) e. ( Base ` K ) /\ U e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) ) -> ( ( ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) <-> ( ( S .\/ T ) .\/ U ) .<_ ( ( P .\/ Q ) .\/ R ) ) )
67 7 20 23 16 66 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) <-> ( ( S .\/ T ) .\/ U ) .<_ ( ( P .\/ Q ) .\/ R ) ) )
68 67 ad3antrrr 
 |-  ( ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( S .\/ T ) .<_ ( ( P .\/ Q ) .\/ R ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) <-> ( ( S .\/ T ) .\/ U ) .<_ ( ( P .\/ Q ) .\/ R ) ) )
69 64 65 68 mpbi2and 
 |-  ( ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( S .\/ T ) .\/ U ) .<_ ( ( P .\/ Q ) .\/ R ) )
70 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( S e. A /\ T e. A /\ U e. A ) )
71 simp12 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( P e. A /\ Q e. A /\ R e. A ) )
72 simp2rr 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> -. U .<_ ( S .\/ T ) )
73 simp2rl 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> S =/= T )
74 1 2 3 3at 
 |-  ( ( ( K e. HL /\ ( S e. A /\ T e. A /\ U e. A ) /\ ( P e. A /\ Q e. A /\ R e. A ) ) /\ ( -. U .<_ ( S .\/ T ) /\ S =/= T ) ) -> ( ( ( S .\/ T ) .\/ U ) .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( S .\/ T ) .\/ U ) = ( ( P .\/ Q ) .\/ R ) ) )
75 6 70 71 72 73 74 syl32anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( S .\/ T ) .\/ U ) .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( S .\/ T ) .\/ U ) = ( ( P .\/ Q ) .\/ R ) ) )
76 75 ad3antrrr 
 |-  ( ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( S .\/ T ) .\/ U ) .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( S .\/ T ) .\/ U ) = ( ( P .\/ Q ) .\/ R ) ) )
77 69 76 mpbid 
 |-  ( ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( S .\/ T ) .\/ U ) = ( ( P .\/ Q ) .\/ R ) )
78 77 eqcomd 
 |-  ( ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) /\ U .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) )
79 78 ex 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( U .<_ ( ( P .\/ Q ) .\/ R ) -> ( ( P .\/ Q ) .\/ R ) = ( ( S .\/ T ) .\/ U ) ) )
80 79 necon3ad 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) -> -. U .<_ ( ( P .\/ Q ) .\/ R ) ) )
81 53 80 mpd 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> -. U .<_ ( ( P .\/ Q ) .\/ R ) )
82 1 2 3 4 lvoli2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ U e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. U .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) e. V )
83 45 47 49 51 81 82 syl113anc 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) e. V )
84 28 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> W e. V )
85 1 4 lvolcmp 
 |-  ( ( K e. HL /\ ( ( ( P .\/ Q ) .\/ R ) .\/ U ) e. V /\ W e. V ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ W <-> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) = W ) )
86 43 83 84 85 syl3anc 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ W <-> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) = W ) )
87 42 86 mpbid 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) = W )
88 5 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( U e. ( Base ` K ) /\ ( ( S .\/ T ) .\/ U ) e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) ) -> ( U .<_ ( ( S .\/ T ) .\/ U ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) ) )
89 7 23 25 16 88 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( U .<_ ( ( S .\/ T ) .\/ U ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) ) )
90 37 89 mpd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
91 90 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ U ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
92 87 91 eqbrtrrd 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ T .<_ ( ( P .\/ Q ) .\/ R ) ) -> W .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
93 5 2 3 hlatjcl 
 |-  ( ( K e. HL /\ S e. A /\ U e. A ) -> ( S .\/ U ) e. ( Base ` K ) )
94 6 17 21 93 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( S .\/ U ) e. ( Base ` K ) )
95 5 1 2 latlej2 
 |-  ( ( K e. Lat /\ ( S .\/ U ) e. ( Base ` K ) /\ T e. ( Base ` K ) ) -> T .<_ ( ( S .\/ U ) .\/ T ) )
96 7 94 59 95 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> T .<_ ( ( S .\/ U ) .\/ T ) )
97 2 3 hlatj32 
 |-  ( ( K e. HL /\ ( S e. A /\ T e. A /\ U e. A ) ) -> ( ( S .\/ T ) .\/ U ) = ( ( S .\/ U ) .\/ T ) )
98 6 17 18 21 97 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( S .\/ T ) .\/ U ) = ( ( S .\/ U ) .\/ T ) )
99 96 98 breqtrrd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> T .<_ ( ( S .\/ T ) .\/ U ) )
100 5 1 7 59 25 30 99 32 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> T .<_ W )
101 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) /\ T e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ T .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ W ) )
102 7 16 59 30 101 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ T .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ W ) )
103 31 100 102 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ W )
104 103 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ W )
105 6 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> K e. HL )
106 44 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
107 12 18 jca 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( R e. A /\ T e. A ) )
108 107 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( R e. A /\ T e. A ) )
109 48 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> P =/= Q )
110 50 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> -. R .<_ ( P .\/ Q ) )
111 simpr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> -. T .<_ ( ( P .\/ Q ) .\/ R ) )
112 1 2 3 4 lvoli2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ T e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) e. V )
113 106 108 109 110 111 112 syl113anc 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) e. V )
114 28 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> W e. V )
115 1 4 lvolcmp 
 |-  ( ( K e. HL /\ ( ( ( P .\/ Q ) .\/ R ) .\/ T ) e. V /\ W e. V ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ W <-> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) = W ) )
116 105 113 114 115 syl3anc 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ W <-> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) = W ) )
117 104 116 mpbid 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) = W )
118 5 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( T e. ( Base ` K ) /\ ( ( S .\/ T ) .\/ U ) e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) ) -> ( T .<_ ( ( S .\/ T ) .\/ U ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) ) )
119 7 59 25 16 118 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( T .<_ ( ( S .\/ T ) .\/ U ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) ) )
120 99 119 mpd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
121 120 ad2antrr 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ T ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
122 117 121 eqbrtrrd 
 |-  ( ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ -. T .<_ ( ( P .\/ Q ) .\/ R ) ) -> W .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
123 92 122 pm2.61dan 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) -> W .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
124 5 2 3 hlatjcl 
 |-  ( ( K e. HL /\ T e. A /\ U e. A ) -> ( T .\/ U ) e. ( Base ` K ) )
125 6 18 21 124 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( T .\/ U ) e. ( Base ` K ) )
126 5 1 2 latlej1 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ ( T .\/ U ) e. ( Base ` K ) ) -> S .<_ ( S .\/ ( T .\/ U ) ) )
127 7 57 125 126 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> S .<_ ( S .\/ ( T .\/ U ) ) )
128 5 2 latjass 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ T e. ( Base ` K ) /\ U e. ( Base ` K ) ) ) -> ( ( S .\/ T ) .\/ U ) = ( S .\/ ( T .\/ U ) ) )
129 7 57 59 23 128 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( S .\/ T ) .\/ U ) = ( S .\/ ( T .\/ U ) ) )
130 127 129 breqtrrd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> S .<_ ( ( S .\/ T ) .\/ U ) )
131 5 1 7 57 25 30 130 32 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> S .<_ W )
132 5 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) /\ S e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ S .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ W ) )
133 7 16 57 30 132 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ S .<_ W ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ W ) )
134 31 131 133 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ W )
135 134 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ W )
136 6 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> K e. HL )
137 44 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) )
138 12 17 jca 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( R e. A /\ S e. A ) )
139 138 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( R e. A /\ S e. A ) )
140 48 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> P =/= Q )
141 50 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> -. R .<_ ( P .\/ Q ) )
142 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> -. S .<_ ( ( P .\/ Q ) .\/ R ) )
143 1 2 3 4 lvoli2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V )
144 137 139 140 141 142 143 syl113anc 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V )
145 28 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> W e. V )
146 1 4 lvolcmp 
 |-  ( ( K e. HL /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V /\ W e. V ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ W <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = W ) )
147 136 144 145 146 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ W <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = W ) )
148 135 147 mpbid 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = W )
149 5 1 2 latjlej2 
 |-  ( ( K e. Lat /\ ( S e. ( Base ` K ) /\ ( ( S .\/ T ) .\/ U ) e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) ) -> ( S .<_ ( ( S .\/ T ) .\/ U ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) ) )
150 7 57 25 16 149 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( S .<_ ( ( S .\/ T ) .\/ U ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) ) )
151 130 150 mpd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
152 151 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
153 148 152 eqbrtrrd 
 |-  ( ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> W .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
154 123 153 pm2.61dan 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> W .<_ ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) )
155 5 1 7 27 30 35 154 latasymd 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) /\ ( ( S e. A /\ T e. A /\ U e. A ) /\ ( S =/= T /\ -. U .<_ ( S .\/ T ) ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .<_ W /\ ( ( S .\/ T ) .\/ U ) .<_ W /\ ( ( P .\/ Q ) .\/ R ) =/= ( ( S .\/ T ) .\/ U ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ ( ( S .\/ T ) .\/ U ) ) = W )