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

Theorem cdleme22e 33649
Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.  F,  N,  O represent f(z), fz(s), fz(t) respectively. When t  \/ v = p  \/ q, fz(s)  <_ fz(t)  \/ v. (Contributed by NM, 6-Dec-2012.)
Hypotheses
Ref Expression
cdleme22.l  |-  .<_  =  ( le `  K )
cdleme22.j  |-  .\/  =  ( join `  K )
cdleme22.m  |-  ./\  =  ( meet `  K )
cdleme22.a  |-  A  =  ( Atoms `  K )
cdleme22.h  |-  H  =  ( LHyp `  K
)
cdleme22e.u  |-  U  =  ( ( P  .\/  Q )  ./\  W )
cdleme22e.f  |-  F  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W
) ) )
cdleme22e.n  |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W
) ) )
cdleme22e.o  |-  O  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W
) ) )
Assertion
Ref Expression
cdleme22e  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  N  .<_  ( O  .\/  V
) )

Proof of Theorem cdleme22e
StepHypRef Expression
1 cdleme22e.n . . 3  |-  N  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W
) ) )
2 simp1l 1029 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  K  e.  HL )
3 hllat 32667 . . . . 5  |-  ( K  e.  HL  ->  K  e.  Lat )
42, 3syl 17 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  K  e.  Lat )
5 simp21l 1122 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  P  e.  A )
6 simp22l 1124 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  Q  e.  A )
7 eqid 2420 . . . . . 6  |-  ( Base `  K )  =  (
Base `  K )
8 cdleme22.j . . . . . 6  |-  .\/  =  ( join `  K )
9 cdleme22.a . . . . . 6  |-  A  =  ( Atoms `  K )
107, 8, 9hlatjcl 32670 . . . . 5  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
112, 5, 6, 10syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  Q )  e.  ( Base `  K
) )
12 simp1r 1030 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  W  e.  H )
13 simp33l 1132 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  z  e.  A )
14 cdleme22.l . . . . . . 7  |-  .<_  =  ( le `  K )
15 cdleme22.m . . . . . . 7  |-  ./\  =  ( meet `  K )
16 cdleme22.h . . . . . . 7  |-  H  =  ( LHyp `  K
)
17 cdleme22e.u . . . . . . 7  |-  U  =  ( ( P  .\/  Q )  ./\  W )
18 cdleme22e.f . . . . . . 7  |-  F  =  ( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W
) ) )
1914, 8, 15, 9, 16, 17, 18, 7cdleme1b 33530 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A  /\  z  e.  A ) )  ->  F  e.  ( Base `  K ) )
202, 12, 5, 6, 13, 19syl23anc 1271 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  F  e.  ( Base `  K
) )
21 simp23l 1126 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  S  e.  A )
227, 8, 9hlatjcl 32670 . . . . . . 7  |-  ( ( K  e.  HL  /\  S  e.  A  /\  z  e.  A )  ->  ( S  .\/  z
)  e.  ( Base `  K ) )
232, 21, 13, 22syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( S  .\/  z )  e.  ( Base `  K
) )
247, 16lhpbase 33301 . . . . . . 7  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
2512, 24syl 17 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  W  e.  ( Base `  K
) )
267, 15latmcl 16242 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( S  .\/  z )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( S  .\/  z )  ./\  W )  e.  ( Base `  K ) )
274, 23, 25, 26syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( S  .\/  z
)  ./\  W )  e.  ( Base `  K
) )
287, 8latjcl 16241 . . . . 5  |-  ( ( K  e.  Lat  /\  F  e.  ( Base `  K )  /\  (
( S  .\/  z
)  ./\  W )  e.  ( Base `  K
) )  ->  ( F  .\/  ( ( S 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)
294, 20, 27, 28syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( F  .\/  ( ( S 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)
307, 14, 15latmle1 16266 . . . 4  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
)  /\  ( F  .\/  ( ( S  .\/  z )  ./\  W
) )  e.  (
Base `  K )
)  ->  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( S  .\/  z ) 
./\  W ) ) )  .<_  ( P  .\/  Q ) )
314, 11, 29, 30syl3anc 1264 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  ./\  ( F  .\/  ( ( S  .\/  z )  ./\  W
) ) )  .<_  ( P  .\/  Q ) )
321, 31syl5eqbr 4450 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  N  .<_  ( P  .\/  Q
) )
33 simp1 1005 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
34 simp21 1038 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
35 simp23r 1127 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  T  e.  A )
36 simp31 1041 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( V  e.  A  /\  V  .<_  W ) )
37 simp32l 1130 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  P  =/=  Q )
38 simp32r 1131 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( T  .\/  V )  =  ( P  .\/  Q
) )
3914, 8, 15, 9, 16, 17cdleme22a 33645 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  Q  e.  A  /\  T  e.  A )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  P  =/= 
Q  /\  ( T  .\/  V )  =  ( P  .\/  Q ) ) )  ->  V  =  U )
4033, 34, 6, 35, 36, 37, 38, 39syl133anc 1287 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  V  =  U )
4140oveq2d 6312 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( O  .\/  V )  =  ( O  .\/  U
) )
42 cdleme22e.o . . . . . 6  |-  O  =  ( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W
) ) )
4342oveq1i 6306 . . . . 5  |-  ( O 
.\/  U )  =  ( ( ( P 
.\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z ) 
./\  W ) ) )  .\/  U )
44 simp21r 1123 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  -.  P  .<_  W )
4514, 8, 15, 9, 16, 17cdleme0a 33515 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  P  =/=  Q ) )  ->  U  e.  A
)
462, 12, 5, 44, 6, 37, 45syl222anc 1280 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  U  e.  A )
477, 8, 9hlatjcl 32670 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  T  e.  A  /\  z  e.  A )  ->  ( T  .\/  z
)  e.  ( Base `  K ) )
482, 35, 13, 47syl3anc 1264 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( T  .\/  z )  e.  ( Base `  K
) )
497, 15latmcl 16242 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( T  .\/  z )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( T  .\/  z )  ./\  W )  e.  ( Base `  K ) )
504, 48, 25, 49syl3anc 1264 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( T  .\/  z
)  ./\  W )  e.  ( Base `  K
) )
517, 8latjcl 16241 . . . . . . 7  |-  ( ( K  e.  Lat  /\  F  e.  ( Base `  K )  /\  (
( T  .\/  z
)  ./\  W )  e.  ( Base `  K
) )  ->  ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)
524, 20, 50, 51syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)
5314, 8, 15, 9, 16, 17cdlemeulpq 33524 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  Q  e.  A ) )  ->  U  .<_  ( P  .\/  Q ) )
542, 12, 5, 6, 53syl22anc 1265 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  U  .<_  ( P  .\/  Q
) )
557, 14, 8, 15, 9atmod2i1 33164 . . . . . 6  |-  ( ( K  e.  HL  /\  ( U  e.  A  /\  ( P  .\/  Q
)  e.  ( Base `  K )  /\  ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)  /\  U  .<_  ( P  .\/  Q ) )  ->  ( (
( P  .\/  Q
)  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W
) ) )  .\/  U )  =  ( ( P  .\/  Q ) 
./\  ( ( F 
.\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) ) )
562, 46, 11, 52, 54, 55syl131anc 1277 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( ( P  .\/  Q )  ./\  ( F  .\/  ( ( T  .\/  z )  ./\  W
) ) )  .\/  U )  =  ( ( P  .\/  Q ) 
./\  ( ( F 
.\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) ) )
5743, 56syl5req 2474 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  ./\  ( ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) )  =  ( O  .\/  U ) )
5841, 57eqtr4d 2464 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( O  .\/  V )  =  ( ( P  .\/  Q )  ./\  ( ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) ) )
5940oveq2d 6312 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( T  .\/  V )  =  ( T  .\/  U
) )
6038, 59eqtr3d 2463 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  Q )  =  ( T  .\/  U
) )
617, 8, 9hlatjcl 32670 . . . . . . . 8  |-  ( ( K  e.  HL  /\  T  e.  A  /\  U  e.  A )  ->  ( T  .\/  U
)  e.  ( Base `  K ) )
622, 35, 46, 61syl3anc 1264 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( T  .\/  U )  e.  ( Base `  K
) )
637, 9atbase 32593 . . . . . . . 8  |-  ( z  e.  A  ->  z  e.  ( Base `  K
) )
6413, 63syl 17 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  z  e.  ( Base `  K
) )
657, 14, 8latlej1 16250 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( T  .\/  U )  e.  ( Base `  K
)  /\  z  e.  ( Base `  K )
)  ->  ( T  .\/  U )  .<_  ( ( T  .\/  U ) 
.\/  z ) )
664, 62, 64, 65syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( T  .\/  U )  .<_  ( ( T  .\/  U )  .\/  z ) )
678, 9hlatj32 32675 . . . . . . . 8  |-  ( ( K  e.  HL  /\  ( T  e.  A  /\  U  e.  A  /\  z  e.  A
) )  ->  (
( T  .\/  U
)  .\/  z )  =  ( ( T 
.\/  z )  .\/  U ) )
682, 35, 46, 13, 67syl13anc 1266 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( T  .\/  U
)  .\/  z )  =  ( ( T 
.\/  z )  .\/  U ) )
697, 9atbase 32593 . . . . . . . . . 10  |-  ( U  e.  A  ->  U  e.  ( Base `  K
) )
7046, 69syl 17 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  U  e.  ( Base `  K
) )
717, 8latj32 16287 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  ( z  e.  (
Base `  K )  /\  U  e.  ( Base `  K )  /\  ( ( T  .\/  z )  ./\  W
)  e.  ( Base `  K ) ) )  ->  ( ( z 
.\/  U )  .\/  ( ( T  .\/  z )  ./\  W
) )  =  ( ( z  .\/  (
( T  .\/  z
)  ./\  W )
)  .\/  U )
)
724, 64, 70, 50, 71syl13anc 1266 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( z  .\/  U
)  .\/  ( ( T  .\/  z )  ./\  W ) )  =  ( ( z  .\/  (
( T  .\/  z
)  ./\  W )
)  .\/  U )
)
737, 8latj32 16287 . . . . . . . . . 10  |-  ( ( K  e.  Lat  /\  ( F  e.  ( Base `  K )  /\  ( ( T  .\/  z )  ./\  W
)  e.  ( Base `  K )  /\  U  e.  ( Base `  K
) ) )  -> 
( ( F  .\/  ( ( T  .\/  z )  ./\  W
) )  .\/  U
)  =  ( ( F  .\/  U ) 
.\/  ( ( T 
.\/  z )  ./\  W ) ) )
744, 20, 50, 70, 73syl13anc 1266 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( F  .\/  (
( T  .\/  z
)  ./\  W )
)  .\/  U )  =  ( ( F 
.\/  U )  .\/  ( ( T  .\/  z )  ./\  W
) ) )
757, 8, 9hlatjcl 32670 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  HL  /\  P  e.  A  /\  z  e.  A )  ->  ( P  .\/  z
)  e.  ( Base `  K ) )
762, 5, 13, 75syl3anc 1264 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  z )  e.  ( Base `  K
) )
7714, 8, 9hlatlej1 32678 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  HL  /\  P  e.  A  /\  z  e.  A )  ->  P  .<_  ( P  .\/  z ) )
782, 5, 13, 77syl3anc 1264 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  P  .<_  ( P  .\/  z
) )
797, 14, 8, 15, 9atmod3i1 33167 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  ( P  .\/  z
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  P  .<_  ( P  .\/  z
) )  ->  ( P  .\/  ( ( P 
.\/  z )  ./\  W ) )  =  ( ( P  .\/  z
)  ./\  ( P  .\/  W ) ) )
802, 5, 76, 25, 78, 79syl131anc 1277 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  ( ( P 
.\/  z )  ./\  W ) )  =  ( ( P  .\/  z
)  ./\  ( P  .\/  W ) ) )
81 eqid 2420 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1.
`  K )  =  ( 1. `  K
)
8214, 8, 81, 9, 16lhpjat2 33324 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  .\/  W
)  =  ( 1.
`  K ) )
832, 12, 34, 82syl21anc 1263 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  W )  =  ( 1. `  K
) )
8483oveq2d 6312 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  z
)  ./\  ( P  .\/  W ) )  =  ( ( P  .\/  z )  ./\  ( 1. `  K ) ) )
85 hlol 32665 . . . . . . . . . . . . . . . . . . 19  |-  ( K  e.  HL  ->  K  e.  OL )
862, 85syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  K  e.  OL )
877, 15, 81olm11 32531 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  OL  /\  ( P  .\/  z )  e.  ( Base `  K
) )  ->  (
( P  .\/  z
)  ./\  ( 1. `  K ) )  =  ( P  .\/  z
) )
8886, 76, 87syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  z
)  ./\  ( 1. `  K ) )  =  ( P  .\/  z
) )
8980, 84, 883eqtrd 2465 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  ( ( P 
.\/  z )  ./\  W ) )  =  ( P  .\/  z ) )
9089oveq1d 6311 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  (
( P  .\/  z
)  ./\  W )
)  .\/  Q )  =  ( ( P 
.\/  z )  .\/  Q ) )
9117oveq2i 6307 . . . . . . . . . . . . . . . . . . 19  |-  ( Q 
.\/  U )  =  ( Q  .\/  (
( P  .\/  Q
)  ./\  W )
)
9214, 8, 9hlatlej2 32679 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  Q  .<_  ( P  .\/  Q ) )
932, 5, 6, 92syl3anc 1264 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  Q  .<_  ( P  .\/  Q
) )
947, 14, 8, 15, 9atmod3i1 33167 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K  e.  HL  /\  ( Q  e.  A  /\  ( P  .\/  Q
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  Q  .<_  ( P  .\/  Q
) )  ->  ( Q  .\/  ( ( P 
.\/  Q )  ./\  W ) )  =  ( ( P  .\/  Q
)  ./\  ( Q  .\/  W ) ) )
952, 6, 11, 25, 93, 94syl131anc 1277 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( Q  .\/  ( ( P 
.\/  Q )  ./\  W ) )  =  ( ( P  .\/  Q
)  ./\  ( Q  .\/  W ) ) )
9691, 95syl5eq 2473 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( Q  .\/  U )  =  ( ( P  .\/  Q )  ./\  ( Q  .\/  W ) ) )
97 simp22 1039 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
9814, 8, 81, 9, 16lhpjat2 33324 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  -> 
( Q  .\/  W
)  =  ( 1.
`  K ) )
992, 12, 97, 98syl21anc 1263 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( Q  .\/  W )  =  ( 1. `  K
) )
10099oveq2d 6312 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  ./\  ( Q  .\/  W ) )  =  ( ( P  .\/  Q )  ./\  ( 1. `  K ) ) )
1017, 15, 81olm11 32531 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  OL  /\  ( P  .\/  Q )  e.  ( Base `  K
) )  ->  (
( P  .\/  Q
)  ./\  ( 1. `  K ) )  =  ( P  .\/  Q
) )
10286, 11, 101syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  ./\  ( 1. `  K ) )  =  ( P  .\/  Q
) )
10396, 100, 1023eqtrd 2465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( Q  .\/  U )  =  ( P  .\/  Q
) )
104103oveq1d 6311 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( Q  .\/  U
)  .\/  ( ( P  .\/  z )  ./\  W ) )  =  ( ( P  .\/  Q
)  .\/  ( ( P  .\/  z )  ./\  W ) ) )
1057, 9atbase 32593 . . . . . . . . . . . . . . . . . 18  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
1065, 105syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  P  e.  ( Base `  K
) )
1077, 15latmcl 16242 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Lat  /\  ( P  .\/  z )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( P  .\/  z )  ./\  W )  e.  ( Base `  K ) )
1084, 76, 25, 107syl3anc 1264 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  z
)  ./\  W )  e.  ( Base `  K
) )
1097, 9atbase 32593 . . . . . . . . . . . . . . . . . 18  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
1106, 109syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  Q  e.  ( Base `  K
) )
1117, 8latj32 16287 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  ( ( P  .\/  z )  ./\  W
)  e.  ( Base `  K )  /\  Q  e.  ( Base `  K
) ) )  -> 
( ( P  .\/  ( ( P  .\/  z )  ./\  W
) )  .\/  Q
)  =  ( ( P  .\/  Q ) 
.\/  ( ( P 
.\/  z )  ./\  W ) ) )
1124, 106, 108, 110, 111syl13anc 1266 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  (
( P  .\/  z
)  ./\  W )
)  .\/  Q )  =  ( ( P 
.\/  Q )  .\/  ( ( P  .\/  z )  ./\  W
) ) )
113104, 112eqtr4d 2464 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( Q  .\/  U
)  .\/  ( ( P  .\/  z )  ./\  W ) )  =  ( ( P  .\/  (
( P  .\/  z
)  ./\  W )
)  .\/  Q )
)
1148, 9hlatj32 32675 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  Q  e.  A  /\  z  e.  A
) )  ->  (
( P  .\/  Q
)  .\/  z )  =  ( ( P 
.\/  z )  .\/  Q ) )
1152, 5, 6, 13, 114syl13anc 1266 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  .\/  z )  =  ( ( P 
.\/  z )  .\/  Q ) )
11690, 113, 1153eqtr4rd 2472 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  .\/  z )  =  ( ( Q 
.\/  U )  .\/  ( ( P  .\/  z )  ./\  W
) ) )
1177, 8latj32 16287 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Lat  /\  ( Q  e.  ( Base `  K )  /\  U  e.  ( Base `  K )  /\  (
( P  .\/  z
)  ./\  W )  e.  ( Base `  K
) ) )  -> 
( ( Q  .\/  U )  .\/  ( ( P  .\/  z ) 
./\  W ) )  =  ( ( Q 
.\/  ( ( P 
.\/  z )  ./\  W ) )  .\/  U
) )
1184, 110, 70, 108, 117syl13anc 1266 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( Q  .\/  U
)  .\/  ( ( P  .\/  z )  ./\  W ) )  =  ( ( Q  .\/  (
( P  .\/  z
)  ./\  W )
)  .\/  U )
)
119116, 118eqtrd 2461 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  .\/  z )  =  ( ( Q 
.\/  ( ( P 
.\/  z )  ./\  W ) )  .\/  U
) )
120119oveq2d 6312 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( z  .\/  U
)  ./\  ( ( P  .\/  Q )  .\/  z ) )  =  ( ( z  .\/  U )  ./\  ( ( Q  .\/  ( ( P 
.\/  z )  ./\  W ) )  .\/  U
) ) )
1217, 8latjcl 16241 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
)  /\  z  e.  ( Base `  K )
)  ->  ( ( P  .\/  Q )  .\/  z )  e.  (
Base `  K )
)
1224, 11, 64, 121syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  .\/  z )  e.  ( Base `  K
) )
1237, 14, 8latlej2 16251 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
)  /\  z  e.  ( Base `  K )
)  ->  z  .<_  ( ( P  .\/  Q
)  .\/  z )
)
1244, 11, 64, 123syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  z  .<_  ( ( P  .\/  Q )  .\/  z ) )
1257, 14, 8, 15, 9atmod1i1 33160 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( z  e.  A  /\  U  e.  ( Base `  K )  /\  ( ( P  .\/  Q )  .\/  z )  e.  ( Base `  K
) )  /\  z  .<_  ( ( P  .\/  Q )  .\/  z ) )  ->  ( z  .\/  ( U  ./\  (
( P  .\/  Q
)  .\/  z )
) )  =  ( ( z  .\/  U
)  ./\  ( ( P  .\/  Q )  .\/  z ) ) )
1262, 13, 70, 122, 124, 125syl131anc 1277 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
z  .\/  ( U  ./\  ( ( P  .\/  Q )  .\/  z ) ) )  =  ( ( z  .\/  U
)  ./\  ( ( P  .\/  Q )  .\/  z ) ) )
12718oveq1i 6306 . . . . . . . . . . . . 13  |-  ( F 
.\/  U )  =  ( ( ( z 
.\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z ) 
./\  W ) ) )  .\/  U )
1287, 8, 9hlatjcl 32670 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  z  e.  A  /\  U  e.  A )  ->  ( z  .\/  U
)  e.  ( Base `  K ) )
1292, 13, 46, 128syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
z  .\/  U )  e.  ( Base `  K
) )
1307, 8latjcl 16241 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Lat  /\  Q  e.  ( Base `  K )  /\  (
( P  .\/  z
)  ./\  W )  e.  ( Base `  K
) )  ->  ( Q  .\/  ( ( P 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)
1314, 110, 108, 130syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( Q  .\/  ( ( P 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)
13214, 8, 9hlatlej2 32679 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  z  e.  A  /\  U  e.  A )  ->  U  .<_  ( z  .\/  U ) )
1332, 13, 46, 132syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  U  .<_  ( z  .\/  U
) )
1347, 14, 8, 15, 9atmod2i1 33164 . . . . . . . . . . . . . 14  |-  ( ( K  e.  HL  /\  ( U  e.  A  /\  ( z  .\/  U
)  e.  ( Base `  K )  /\  ( Q  .\/  ( ( P 
.\/  z )  ./\  W ) )  e.  (
Base `  K )
)  /\  U  .<_  ( z  .\/  U ) )  ->  ( (
( z  .\/  U
)  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W
) ) )  .\/  U )  =  ( ( z  .\/  U ) 
./\  ( ( Q 
.\/  ( ( P 
.\/  z )  ./\  W ) )  .\/  U
) ) )
1352, 46, 129, 131, 133, 134syl131anc 1277 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( ( z  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  z )  ./\  W
) ) )  .\/  U )  =  ( ( z  .\/  U ) 
./\  ( ( Q 
.\/  ( ( P 
.\/  z )  ./\  W ) )  .\/  U
) ) )
136127, 135syl5eq 2473 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( F  .\/  U )  =  ( ( z  .\/  U )  ./\  ( ( Q  .\/  ( ( P 
.\/  z )  ./\  W ) )  .\/  U
) ) )
137120, 126, 1363eqtr4rd 2472 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( F  .\/  U )  =  ( z  .\/  ( U  ./\  ( ( P 
.\/  Q )  .\/  z ) ) ) )
1387, 14, 8latlej1 16250 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
)  /\  z  e.  ( Base `  K )
)  ->  ( P  .\/  Q )  .<_  ( ( P  .\/  Q ) 
.\/  z ) )
1394, 11, 64, 138syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  Q )  .<_  ( ( P  .\/  Q )  .\/  z ) )
1407, 14, 4, 70, 11, 122, 54, 139lattrd 16248 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  U  .<_  ( ( P  .\/  Q )  .\/  z ) )
1417, 14, 15latleeqm1 16269 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Lat  /\  U  e.  ( Base `  K )  /\  (
( P  .\/  Q
)  .\/  z )  e.  ( Base `  K
) )  ->  ( U  .<_  ( ( P 
.\/  Q )  .\/  z )  <->  ( U  ./\  ( ( P  .\/  Q )  .\/  z ) )  =  U ) )
1424, 70, 122, 141syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( U  .<_  ( ( P 
.\/  Q )  .\/  z )  <->  ( U  ./\  ( ( P  .\/  Q )  .\/  z ) )  =  U ) )
143140, 142mpbid 213 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( U  ./\  ( ( P 
.\/  Q )  .\/  z ) )  =  U )
144143oveq2d 6312 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
z  .\/  ( U  ./\  ( ( P  .\/  Q )  .\/  z ) ) )  =  ( z  .\/  U ) )
145137, 144eqtrd 2461 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( F  .\/  U )  =  ( z  .\/  U
) )
146145oveq1d 6311 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( F  .\/  U
)  .\/  ( ( T  .\/  z )  ./\  W ) )  =  ( ( z  .\/  U
)  .\/  ( ( T  .\/  z )  ./\  W ) ) )
14774, 146eqtrd 2461 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( F  .\/  (
( T  .\/  z
)  ./\  W )
)  .\/  U )  =  ( ( z 
.\/  U )  .\/  ( ( T  .\/  z )  ./\  W
) ) )
14814, 8, 9hlatlej2 32679 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  T  e.  A  /\  z  e.  A )  ->  z  .<_  ( T  .\/  z ) )
1492, 35, 13, 148syl3anc 1264 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  z  .<_  ( T  .\/  z
) )
1507, 14, 8, 15, 9atmod3i1 33167 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( z  e.  A  /\  ( T  .\/  z
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  z  .<_  ( T  .\/  z
) )  ->  (
z  .\/  ( ( T  .\/  z )  ./\  W ) )  =  ( ( T  .\/  z
)  ./\  ( z  .\/  W ) ) )
1512, 13, 48, 25, 149, 150syl131anc 1277 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
z  .\/  ( ( T  .\/  z )  ./\  W ) )  =  ( ( T  .\/  z
)  ./\  ( z  .\/  W ) ) )
152 simp33 1043 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
z  e.  A  /\  -.  z  .<_  W ) )
15314, 8, 81, 9, 16lhpjat2 33324 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( z  e.  A  /\  -.  z  .<_  W ) )  -> 
( z  .\/  W
)  =  ( 1.
`  K ) )
1542, 12, 152, 153syl21anc 1263 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
z  .\/  W )  =  ( 1. `  K ) )
155154oveq2d 6312 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( T  .\/  z
)  ./\  ( z  .\/  W ) )  =  ( ( T  .\/  z )  ./\  ( 1. `  K ) ) )
156151, 155eqtrd 2461 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
z  .\/  ( ( T  .\/  z )  ./\  W ) )  =  ( ( T  .\/  z
)  ./\  ( 1. `  K ) ) )
1577, 15, 81olm11 32531 . . . . . . . . . . 11  |-  ( ( K  e.  OL  /\  ( T  .\/  z )  e.  ( Base `  K
) )  ->  (
( T  .\/  z
)  ./\  ( 1. `  K ) )  =  ( T  .\/  z
) )
15886, 48, 157syl2anc 665 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( T  .\/  z
)  ./\  ( 1. `  K ) )  =  ( T  .\/  z
) )
159156, 158eqtr2d 2462 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( T  .\/  z )  =  ( z  .\/  (
( T  .\/  z
)  ./\  W )
) )
160159oveq1d 6311 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( T  .\/  z
)  .\/  U )  =  ( ( z 
.\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) )
16172, 147, 1603eqtr4rd 2472 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( T  .\/  z
)  .\/  U )  =  ( ( F 
.\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) )
16268, 161eqtrd 2461 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( T  .\/  U
)  .\/  z )  =  ( ( F 
.\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) )
16366, 162breqtrd 4441 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( T  .\/  U )  .<_  ( ( F  .\/  ( ( T  .\/  z )  ./\  W
) )  .\/  U
) )
16460, 163eqbrtrd 4437 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  Q )  .<_  ( ( F  .\/  ( ( T  .\/  z )  ./\  W
) )  .\/  U
) )
1657, 8latjcl 16241 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( F  .\/  ( ( T  .\/  z ) 
./\  W ) )  e.  ( Base `  K
)  /\  U  e.  ( Base `  K )
)  ->  ( ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
)  e.  ( Base `  K ) )
1664, 52, 70, 165syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( F  .\/  (
( T  .\/  z
)  ./\  W )
)  .\/  U )  e.  ( Base `  K
) )
1677, 14, 15latleeqm1 16269 . . . . 5  |-  ( ( K  e.  Lat  /\  ( P  .\/  Q )  e.  ( Base `  K
)  /\  ( ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
)  e.  ( Base `  K ) )  -> 
( ( P  .\/  Q )  .<_  ( ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
)  <->  ( ( P 
.\/  Q )  ./\  ( ( F  .\/  ( ( T  .\/  z )  ./\  W
) )  .\/  U
) )  =  ( P  .\/  Q ) ) )
1684, 11, 166, 167syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  .<_  ( ( F 
.\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
)  <->  ( ( P 
.\/  Q )  ./\  ( ( F  .\/  ( ( T  .\/  z )  ./\  W
) )  .\/  U
) )  =  ( P  .\/  Q ) ) )
169164, 168mpbid 213 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  (
( P  .\/  Q
)  ./\  ( ( F  .\/  ( ( T 
.\/  z )  ./\  W ) )  .\/  U
) )  =  ( P  .\/  Q ) )
17058, 169eqtr2d 2462 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  ( P  .\/  Q )  =  ( O  .\/  V
) )
17132, 170breqtrd 4441 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( S  e.  A  /\  T  e.  A ) )  /\  ( ( V  e.  A  /\  V  .<_  W )  /\  ( P  =/=  Q  /\  ( T  .\/  V )  =  ( P  .\/  Q
) )  /\  (
z  e.  A  /\  -.  z  .<_  W ) ) )  ->  N  .<_  ( O  .\/  V
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1867    =/= wne 2616   class class class wbr 4417   ` cfv 5592  (class class class)co 6296   Basecbs 15073   lecple 15149   joincjn 16133   meetcmee 16134   1.cp1 16228   Latclat 16235   OLcol 32478   Atomscatm 32567   HLchlt 32654   LHypclh 33287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6798  df-2nd 6799  df-preset 16117  df-poset 16135  df-plt 16148  df-lub 16164  df-glb 16165  df-join 16166  df-meet 16167  df-p0 16229  df-p1 16230  df-lat 16236  df-clat 16298  df-oposet 32480  df-ol 32482  df-oml 32483  df-covers 32570  df-ats 32571  df-atl 32602  df-cvlat 32626  df-hlat 32655  df-psubsp 32806  df-pmap 32807  df-padd 33099  df-lhyp 33291
This theorem is referenced by:  cdleme26e  33664
  Copyright terms: Public domain W3C validator