Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2lplnja Unicode version

Theorem 2lplnja 29808
Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 29809 in terms of atoms). (Contributed by NM, 12-Jul-2012.)
Hypotheses
Ref Expression
2lplnja.l  |-  .<_  =  ( le `  K )
2lplnja.j  |-  .\/  =  ( join `  K )
2lplnja.a  |-  A  =  ( Atoms `  K )
2lplnja.v  |-  V  =  ( LVols `  K )
Assertion
Ref Expression
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 of Theorem 2lplnja
StepHypRef Expression
1 eqid 2283 . 2  |-  ( Base `  K )  =  (
Base `  K )
2 2lplnja.l . 2  |-  .<_  =  ( le `  K )
3 simp11l 1066 . . 3  |-  ( ( ( ( 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 )
4 hllat 29553 . . 3  |-  ( K  e.  HL  ->  K  e.  Lat )
53, 4syl 15 . 2  |-  ( ( ( ( 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 )
6 simp121 1087 . . . . 5  |-  ( ( ( ( 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 )
7 simp122 1088 . . . . 5  |-  ( ( ( ( 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 )
8 2lplnja.j . . . . . 6  |-  .\/  =  ( join `  K )
9 2lplnja.a . . . . . 6  |-  A  =  ( Atoms `  K )
101, 8, 9hlatjcl 29556 . . . . 5  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
113, 6, 7, 10syl3anc 1182 . . . 4  |-  ( ( ( ( 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 1089 . . . . 5  |-  ( ( ( ( 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 )
131, 9atbase 29479 . . . . 5  |-  ( R  e.  A  ->  R  e.  ( Base `  K
) )
1412, 13syl 15 . . . 4  |-  ( ( ( ( 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 )
)
151, 8latjcl 14156 . . . 4  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
)  /\  R  e.  ( Base `  K )
)  ->  ( ( P  .\/  Q )  .\/  R )  e.  ( Base `  K ) )
165, 11, 14, 15syl3anc 1182 . . 3  |-  ( ( ( ( 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 1054 . . . . 5  |-  ( ( ( ( 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 1055 . . . . 5  |-  ( ( ( ( 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 )
191, 8, 9hlatjcl 29556 . . . . 5  |-  ( ( K  e.  HL  /\  S  e.  A  /\  T  e.  A )  ->  ( S  .\/  T
)  e.  ( Base `  K ) )
203, 17, 18, 19syl3anc 1182 . . . 4  |-  ( ( ( ( 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 1056 . . . . 5  |-  ( ( ( ( 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 )
221, 9atbase 29479 . . . . 5  |-  ( U  e.  A  ->  U  e.  ( Base `  K
) )
2321, 22syl 15 . . . 4  |-  ( ( ( ( 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 )
)
241, 8latjcl 14156 . . . 4  |-  ( ( K  e.  Lat  /\  ( S  .\/  T )  e.  ( Base `  K
)  /\  U  e.  ( Base `  K )
)  ->  ( ( S  .\/  T )  .\/  U )  e.  ( Base `  K ) )
255, 20, 23, 24syl3anc 1182 . . 3  |-  ( ( ( ( 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 ) )
261, 8latjcl 14156 . . 3  |-  ( ( K  e.  Lat  /\  ( ( P  .\/  Q )  .\/  R )  e.  ( Base `  K
)  /\  ( ( S  .\/  T )  .\/  U )  e.  ( Base `  K ) )  -> 
( ( ( P 
.\/  Q )  .\/  R )  .\/  ( ( S  .\/  T ) 
.\/  U ) )  e.  ( Base `  K
) )
275, 16, 25, 26syl3anc 1182 . 2  |-  ( ( ( ( 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 1067 . . 3  |-  ( ( ( ( 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 2lplnja.v . . . 4  |-  V  =  ( LVols `  K )
301, 29lvolbase 29767 . . 3  |-  ( W  e.  V  ->  W  e.  ( Base `  K
) )
3128, 30syl 15 . 2  |-  ( ( ( ( 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 )
)
32 simp31 991 . . 3  |-  ( ( ( ( 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 )
33 simp32 992 . . 3  |-  ( ( ( ( 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 )
341, 2, 8latjle12 14168 . . . 4  |-  ( ( 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 )
)
355, 16, 25, 31, 34syl13anc 1184 . . 3  |-  ( ( ( ( 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 )
)
3632, 33, 35mpbi2and 887 . 2  |-  ( ( ( ( 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 )
371, 2, 8latlej2 14167 . . . . . . . . . 10  |-  ( ( K  e.  Lat  /\  ( S  .\/  T )  e.  ( Base `  K
)  /\  U  e.  ( Base `  K )
)  ->  U  .<_  ( ( S  .\/  T
)  .\/  U )
)
385, 20, 23, 37syl3anc 1182 . . . . . . . . 9  |-  ( ( ( ( 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 )
)
391, 2, 5, 23, 25, 31, 38, 33lattrd 14164 . . . . . . . 8  |-  ( ( ( ( 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 )
401, 2, 8latjle12 14168 . . . . . . . . 9  |-  ( ( 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 ) )
415, 16, 23, 31, 40syl13anc 1184 . . . . . . . 8  |-  ( ( ( ( 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 )
)
4232, 39, 41mpbi2and 887 . . . . . . 7  |-  ( ( ( ( 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 )
4342ad2antrr 706 . . . . . 6  |-  ( ( ( ( ( ( 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 )
443ad2antrr 706 . . . . . . 7  |-  ( ( ( ( ( ( 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 )
453, 6, 73jca 1132 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
4645ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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 ) )
4712, 21jca 518 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
4847ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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 ) )
49 simp13l 1070 . . . . . . . . 9  |-  ( ( ( ( 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 )
5049ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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 )
51 simp13r 1071 . . . . . . . . 9  |-  ( ( ( ( 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
) )
5251ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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
) )
53 simp33 993 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
5453ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ( ( ( 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 ) )
55 simplr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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 )
)
56 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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 )
)
571, 9atbase 29479 . . . . . . . . . . . . . . . . . . 19  |-  ( S  e.  A  ->  S  e.  ( Base `  K
) )
5817, 57syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
)
591, 9atbase 29479 . . . . . . . . . . . . . . . . . . 19  |-  ( T  e.  A  ->  T  e.  ( Base `  K
) )
6018, 59syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
)
611, 2, 8latjle12 14168 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
625, 58, 60, 16, 61syl13anc 1184 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) )
6362ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( 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 ) ) )
6455, 56, 63mpbi2and 887 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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 ) )
6564adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( 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 ) )
66 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( 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 )
)
671, 2, 8latjle12 14168 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) )
685, 20, 23, 16, 67syl13anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) ) )
6968ad3antrrr 710 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( 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 ) ) )
7065, 66, 69mpbi2and 887 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 ) )
71 simp2l 981 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
72 simp12 986 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
73 simp2rr 1025 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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
) )
74 simp2rl 1024 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
752, 8, 93at 29679 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
763, 71, 72, 73, 74, 75syl32anc 1190 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )
7776ad3antrrr 710 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( 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 ) ) )
7870, 77mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( 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 ) )
7978eqcomd 2288 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( 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 ) )
8079ex 423 . . . . . . . . . 10  |-  ( ( ( ( ( ( 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 ) ) )
8180necon3ad 2482 . . . . . . . . 9  |-  ( ( ( ( ( ( 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 )
) )
8254, 81mpd 14 . . . . . . . 8  |-  ( ( ( ( ( ( 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 ) )
832, 8, 9, 29lvoli2 29770 . . . . . . . 8  |-  ( ( ( 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 )
8446, 48, 50, 52, 82, 83syl113anc 1194 . . . . . . 7  |-  ( ( ( ( ( ( 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
)
8528ad2antrr 706 . . . . . . 7  |-  ( ( ( ( ( ( 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 )
862, 29lvolcmp 29806 . . . . . . 7  |-  ( ( K  e.  HL  /\  ( ( ( P 
.\/  Q )  .\/  R )  .\/  U )  e.  V  /\  W  e.  V )  ->  (
( ( ( P 
.\/  Q )  .\/  R )  .\/  U ) 
.<_  W  <->  ( ( ( P  .\/  Q ) 
.\/  R )  .\/  U )  =  W ) )
8744, 84, 85, 86syl3anc 1182 . . . . . 6  |-  ( ( ( ( ( ( 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 ) )
8843, 87mpbid 201 . . . . 5  |-  ( ( ( ( ( ( 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 )
891, 2, 8latjlej2 14172 . . . . . . . 8  |-  ( ( 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 ) ) ) )
905, 23, 25, 16, 89syl13anc 1184 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) )
9138, 90mpd 14 . . . . . 6  |-  ( ( ( ( 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 ) ) )
9291ad2antrr 706 . . . . 5  |-  ( ( ( ( ( ( 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 ) ) )
9388, 92eqbrtrrd 4045 . . . 4  |-  ( ( ( ( ( ( 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 ) ) )
941, 8, 9hlatjcl 29556 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  S  e.  A  /\  U  e.  A )  ->  ( S  .\/  U
)  e.  ( Base `  K ) )
953, 17, 21, 94syl3anc 1182 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
)
961, 2, 8latlej2 14167 . . . . . . . . . . 11  |-  ( ( K  e.  Lat  /\  ( S  .\/  U )  e.  ( Base `  K
)  /\  T  e.  ( Base `  K )
)  ->  T  .<_  ( ( S  .\/  U
)  .\/  T )
)
975, 95, 60, 96syl3anc 1182 . . . . . . . . . 10  |-  ( ( ( ( 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 )
)
988, 9hlatj32 29561 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  U  e.  A
) )  ->  (
( S  .\/  T
)  .\/  U )  =  ( ( S 
.\/  U )  .\/  T ) )
993, 17, 18, 21, 98syl13anc 1184 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
10097, 99breqtrrd 4049 . . . . . . . . 9  |-  ( ( ( ( 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 )
)
1011, 2, 5, 60, 25, 31, 100, 33lattrd 14164 . . . . . . . 8  |-  ( ( ( ( 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 )
1021, 2, 8latjle12 14168 . . . . . . . . 9  |-  ( ( 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 ) )
1035, 16, 60, 31, 102syl13anc 1184 . . . . . . . 8  |-  ( ( ( ( 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 )
)
10432, 101, 103mpbi2and 887 . . . . . . 7  |-  ( ( ( ( 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 )
105104ad2antrr 706 . . . . . 6  |-  ( ( ( ( ( ( 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 )
1063ad2antrr 706 . . . . . . 7  |-  ( ( ( ( ( ( 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 )
10745ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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 ) )
10812, 18jca 518 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
109108ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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 ) )
11049ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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 )
11151ad2antrr 706 . . . . . . . 8  |-  ( ( ( ( ( ( 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
) )
112 simpr 447 . . . . . . . 8  |-  ( ( ( ( ( ( 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 ) )
1132, 8, 9, 29lvoli2 29770 . . . . . . . 8  |-  ( ( ( 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 )
114107, 109, 110, 111, 112, 113syl113anc 1194 . . . . . . 7  |-  ( ( ( ( ( ( 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
)
11528ad2antrr 706 . . . . . . 7  |-  ( ( ( ( ( ( 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 )
1162, 29lvolcmp 29806 . . . . . . 7  |-  ( ( K  e.  HL  /\  ( ( ( P 
.\/  Q )  .\/  R )  .\/  T )  e.  V  /\  W  e.  V )  ->  (
( ( ( P 
.\/  Q )  .\/  R )  .\/  T ) 
.<_  W  <->  ( ( ( P  .\/  Q ) 
.\/  R )  .\/  T )  =  W ) )
117106, 114, 115, 116syl3anc 1182 . . . . . 6  |-  ( ( ( ( ( ( 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 ) )
118105, 117mpbid 201 . . . . 5  |-  ( ( ( ( ( ( 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 )
1191, 2, 8latjlej2 14172 . . . . . . . 8  |-  ( ( 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 ) ) ) )
1205, 60, 25, 16, 119syl13anc 1184 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) )
121100, 120mpd 14 . . . . . 6  |-  ( ( ( ( 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 ) ) )
122121ad2antrr 706 . . . . 5  |-  ( ( ( ( ( ( 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 ) ) )
123118, 122eqbrtrrd 4045 . . . 4  |-  ( ( ( ( ( ( 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 ) ) )
12493, 123pm2.61dan 766 . . 3  |-  ( ( ( ( ( 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 ) ) )
1251, 8, 9hlatjcl 29556 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  T  e.  A  /\  U  e.  A )  ->  ( T  .\/  U
)  e.  ( Base `  K ) )
1263, 18, 21, 125syl3anc 1182 . . . . . . . . . 10  |-  ( ( ( ( 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 )
)
1271, 2, 8latlej1 14166 . . . . . . . . . 10  |-  ( ( K  e.  Lat  /\  S  e.  ( Base `  K )  /\  ( T  .\/  U )  e.  ( Base `  K
) )  ->  S  .<_  ( S  .\/  ( T  .\/  U ) ) )
1285, 58, 126, 127syl3anc 1182 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
1291, 8latjass 14201 . . . . . . . . . 10  |-  ( ( K  e.  Lat  /\  ( S  e.  ( Base `  K )  /\  T  e.  ( Base `  K )  /\  U  e.  ( Base `  K
) ) )  -> 
( ( S  .\/  T )  .\/  U )  =  ( S  .\/  ( T  .\/  U ) ) )
1305, 58, 60, 23, 129syl13anc 1184 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
131128, 130breqtrrd 4049 . . . . . . . 8  |-  ( ( ( ( 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 )
)
1321, 2, 5, 58, 25, 31, 131, 33lattrd 14164 . . . . . . 7  |-  ( ( ( ( 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 )
1331, 2, 8latjle12 14168 . . . . . . . 8  |-  ( ( 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 ) )
1345, 16, 58, 31, 133syl13anc 1184 . . . . . . 7  |-  ( ( ( ( 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 )
)
13532, 132, 134mpbi2and 887 . . . . . 6  |-  ( ( ( ( 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 )
136135adantr 451 . . . . 5  |-  ( ( ( ( (