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

Theorem dihopelvalcpre 31438
Description: Member of value of isomorphism H for a lattice  K when  -.  X  .<_  W, given auxiliary atom  Q. TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014.)
Hypotheses
Ref Expression
dihopelvalcp.b  |-  B  =  ( Base `  K
)
dihopelvalcp.l  |-  .<_  =  ( le `  K )
dihopelvalcp.j  |-  .\/  =  ( join `  K )
dihopelvalcp.m  |-  ./\  =  ( meet `  K )
dihopelvalcp.a  |-  A  =  ( Atoms `  K )
dihopelvalcp.h  |-  H  =  ( LHyp `  K
)
dihopelvalcp.p  |-  P  =  ( ( oc `  K ) `  W
)
dihopelvalcp.t  |-  T  =  ( ( LTrn `  K
) `  W )
dihopelvalcp.r  |-  R  =  ( ( trL `  K
) `  W )
dihopelvalcp.e  |-  E  =  ( ( TEndo `  K
) `  W )
dihopelvalcp.i  |-  I  =  ( ( DIsoH `  K
) `  W )
dihopelvalcp.g  |-  G  =  ( iota_ g  e.  T
( g `  P
)  =  Q )
dihopelvalcp.f  |-  F  e. 
_V
dihopelvalcp.s  |-  S  e. 
_V
dihopelvalcp.z  |-  Z  =  ( h  e.  T  |->  (  _I  |`  B ) )
dihopelvalcp.n  |-  N  =  ( ( DIsoB `  K
) `  W )
dihopelvalcp.c  |-  C  =  ( ( DIsoC `  K
) `  W )
dihopelvalcp.u  |-  U  =  ( ( DVecH `  K
) `  W )
dihopelvalcp.d  |-  .+  =  ( +g  `  U )
dihopelvalcp.v  |-  V  =  ( LSubSp `  U )
dihopelvalcp.y  |-  .(+)  =  (
LSSum `  U )
dihopelvalcp.o  |-  O  =  ( a  e.  E ,  b  e.  E  |->  ( h  e.  T  |->  ( ( a `  h )  o.  (
b `  h )
) ) )
Assertion
Ref Expression
dihopelvalcpre  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( <. F ,  S >.  e.  ( I `  X )  <-> 
( ( F  e.  T  /\  S  e.  E )  /\  ( R `  ( F  o.  `' ( S `  G ) ) ) 
.<_  X ) ) )
Distinct variable groups:    .<_ , g    A, g    P, g    a, b, E    g, h, H   
g, a, h, K, b    B, h    T, a, b, g, h    W, a, b, g, h    Q, g
Allowed substitution hints:    A( h, a, b)    B( g, a, b)    C( g, h, a, b)    P( h, a, b)    .+ ( g, h, a, b)    .(+) ( g, h, a, b)    Q( h, a, b)    R( g, h, a, b)    S( g, h, a, b)    U( g, h, a, b)    E( g, h)    F( g, h, a, b)    G( g, h, a, b)    H( a, b)    I( g, h, a, b)    .\/ ( g, h, a, b)    .<_ ( h, a, b)    ./\ ( g, h, a, b)    N( g, h, a, b)    O( g, h, a, b)    V( g, h, a, b)    X( g, h, a, b)    Z( g, h, a, b)

Proof of Theorem dihopelvalcpre
Dummy variables  x  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihopelvalcp.b . . . 4  |-  B  =  ( Base `  K
)
2 dihopelvalcp.l . . . 4  |-  .<_  =  ( le `  K )
3 dihopelvalcp.j . . . 4  |-  .\/  =  ( join `  K )
4 dihopelvalcp.m . . . 4  |-  ./\  =  ( meet `  K )
5 dihopelvalcp.a . . . 4  |-  A  =  ( Atoms `  K )
6 dihopelvalcp.h . . . 4  |-  H  =  ( LHyp `  K
)
7 dihopelvalcp.i . . . 4  |-  I  =  ( ( DIsoH `  K
) `  W )
8 dihopelvalcp.n . . . 4  |-  N  =  ( ( DIsoB `  K
) `  W )
9 dihopelvalcp.c . . . 4  |-  C  =  ( ( DIsoC `  K
) `  W )
10 dihopelvalcp.u . . . 4  |-  U  =  ( ( DVecH `  K
) `  W )
11 dihopelvalcp.y . . . 4  |-  .(+)  =  (
LSSum `  U )
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11dihvalcq 31426 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( I `  X )  =  ( ( C `  Q
)  .(+)  ( N `  ( X  ./\  W ) ) ) )
1312eleq2d 2350 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( <. F ,  S >.  e.  ( I `  X )  <->  <. F ,  S >.  e.  ( ( C `  Q )  .(+)  ( N `
 ( X  ./\  W ) ) ) ) )
14 simp1 955 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
15 simp3l 983 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
16 dihopelvalcp.v . . . . 5  |-  V  =  ( LSubSp `  U )
172, 5, 6, 10, 9, 16diclss 31383 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  -> 
( C `  Q
)  e.  V )
1814, 15, 17syl2anc 642 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( C `  Q )  e.  V
)
19 simp1l 979 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  K  e.  HL )
20 hllat 29553 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  Lat )
2119, 20syl 15 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  K  e.  Lat )
22 simp2l 981 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  X  e.  B )
23 simp1r 980 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  W  e.  H )
241, 6lhpbase 30187 . . . . . 6  |-  ( W  e.  H  ->  W  e.  B )
2523, 24syl 15 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  W  e.  B )
261, 4latmcl 14157 . . . . 5  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  W  e.  B )  ->  ( X  ./\  W
)  e.  B )
2721, 22, 25, 26syl3anc 1182 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( X  ./\ 
W )  e.  B
)
281, 2, 4latmle2 14183 . . . . 5  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  W  e.  B )  ->  ( X  ./\  W
)  .<_  W )
2921, 22, 25, 28syl3anc 1182 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( X  ./\ 
W )  .<_  W )
301, 2, 6, 10, 8, 16diblss 31360 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( X 
./\  W )  e.  B  /\  ( X 
./\  W )  .<_  W ) )  -> 
( N `  ( X  ./\  W ) )  e.  V )
3114, 27, 29, 30syl12anc 1180 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( N `  ( X  ./\  W
) )  e.  V
)
32 dihopelvalcp.d . . . 4  |-  .+  =  ( +g  `  U )
336, 10, 32, 16, 11dvhopellsm 31307 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( C `  Q )  e.  V  /\  ( N `  ( X  ./\  W ) )  e.  V )  -> 
( <. F ,  S >.  e.  ( ( C `
 Q )  .(+)  ( N `  ( X 
./\  W ) ) )  <->  E. x E. y E. z E. w ( ( <. x ,  y
>.  e.  ( C `  Q )  /\  <. z ,  w >.  e.  ( N `  ( X 
./\  W ) ) )  /\  <. F ,  S >.  =  ( <.
x ,  y >.  .+  <. z ,  w >. ) ) ) )
3414, 18, 31, 33syl3anc 1182 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( <. F ,  S >.  e.  ( ( C `  Q
)  .(+)  ( N `  ( X  ./\  W ) ) )  <->  E. x E. y E. z E. w ( ( <.
x ,  y >.  e.  ( C `  Q
)  /\  <. z ,  w >.  e.  ( N `  ( X  ./\ 
W ) ) )  /\  <. F ,  S >.  =  ( <. x ,  y >.  .+  <. z ,  w >. )
) ) )
35 dihopelvalcp.p . . . . . . . . 9  |-  P  =  ( ( oc `  K ) `  W
)
36 dihopelvalcp.t . . . . . . . . 9  |-  T  =  ( ( LTrn `  K
) `  W )
37 dihopelvalcp.e . . . . . . . . 9  |-  E  =  ( ( TEndo `  K
) `  W )
38 dihopelvalcp.g . . . . . . . . 9  |-  G  =  ( iota_ g  e.  T
( g `  P
)  =  Q )
39 vex 2791 . . . . . . . . 9  |-  x  e. 
_V
40 vex 2791 . . . . . . . . 9  |-  y  e. 
_V
412, 5, 6, 35, 36, 37, 9, 38, 39, 40dicopelval2 31371 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  -> 
( <. x ,  y
>.  e.  ( C `  Q )  <->  ( x  =  ( y `  G )  /\  y  e.  E ) ) )
4214, 15, 41syl2anc 642 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( <. x ,  y >.  e.  ( C `  Q )  <-> 
( x  =  ( y `  G )  /\  y  e.  E
) ) )
43 dihopelvalcp.r . . . . . . . . 9  |-  R  =  ( ( trL `  K
) `  W )
44 dihopelvalcp.z . . . . . . . . 9  |-  Z  =  ( h  e.  T  |->  (  _I  |`  B ) )
451, 2, 6, 36, 43, 44, 8dibopelval3 31338 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( X 
./\  W )  e.  B  /\  ( X 
./\  W )  .<_  W ) )  -> 
( <. z ,  w >.  e.  ( N `  ( X  ./\  W ) )  <->  ( ( z  e.  T  /\  ( R `  z )  .<_  ( X  ./\  W
) )  /\  w  =  Z ) ) )
4614, 27, 29, 45syl12anc 1180 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( <. z ,  w >.  e.  ( N `  ( X 
./\  W ) )  <-> 
( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )
4742, 46anbi12d 691 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( ( <. x ,  y >.  e.  ( C `  Q
)  /\  <. z ,  w >.  e.  ( N `  ( X  ./\ 
W ) ) )  <-> 
( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) ) )
4847anbi1d 685 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( (
( <. x ,  y
>.  e.  ( C `  Q )  /\  <. z ,  w >.  e.  ( N `  ( X 
./\  W ) ) )  /\  <. F ,  S >.  =  ( <.
x ,  y >.  .+  <. z ,  w >. ) )  <->  ( (
( x  =  ( y `  G )  /\  y  e.  E
)  /\  ( (
z  e.  T  /\  ( R `  z ) 
.<_  ( X  ./\  W
) )  /\  w  =  Z ) )  /\  <. F ,  S >.  =  ( <. x ,  y
>.  .+  <. z ,  w >. ) ) ) )
49 simpl1 958 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
50 simprll 738 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  x  =  ( y `  G ) )
51 simprlr 739 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  y  e.  E
)
522, 5, 6, 35lhpocnel2 30208 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
5349, 52syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
54 simpl3l 1010 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
552, 5, 6, 36, 38ltrniotacl 30768 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  G  e.  T )
5649, 53, 54, 55syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  G  e.  T
)
576, 36, 37tendocl 30956 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  y  e.  E  /\  G  e.  T
)  ->  ( y `  G )  e.  T
)
5849, 51, 56, 57syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( y `  G )  e.  T
)
5950, 58eqeltrd 2357 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  x  e.  T
)
60 simprll 738 . . . . . . . . . . . 12  |-  ( ( ( x  =  ( y `  G )  /\  y  e.  E
)  /\  ( (
z  e.  T  /\  ( R `  z ) 
.<_  ( X  ./\  W
) )  /\  w  =  Z ) )  -> 
z  e.  T )
6160adantl 452 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  z  e.  T
)
62 simprrr 741 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  w  =  Z )
631, 6, 36, 37, 44tendo0cl 30979 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  Z  e.  E )
6449, 63syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  Z  e.  E
)
6562, 64eqeltrd 2357 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  w  e.  E
)
66 eqid 2283 . . . . . . . . . . . 12  |-  (Scalar `  U )  =  (Scalar `  U )
67 eqid 2283 . . . . . . . . . . . 12  |-  ( +g  `  (Scalar `  U )
)  =  ( +g  `  (Scalar `  U )
)
686, 36, 37, 10, 66, 32, 67dvhopvadd 31283 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( x  e.  T  /\  y  e.  E )  /\  (
z  e.  T  /\  w  e.  E )
)  ->  ( <. x ,  y >.  .+  <. z ,  w >. )  =  <. ( x  o.  z ) ,  ( y ( +g  `  (Scalar `  U ) ) w ) >. )
6949, 59, 51, 61, 65, 68syl122anc 1191 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( <. x ,  y >.  .+  <. z ,  w >. )  =  <. ( x  o.  z ) ,  ( y ( +g  `  (Scalar `  U ) ) w ) >. )
70 dihopelvalcp.o . . . . . . . . . . . . . 14  |-  O  =  ( a  e.  E ,  b  e.  E  |->  ( h  e.  T  |->  ( ( a `  h )  o.  (
b `  h )
) ) )
716, 36, 37, 10, 66, 70, 67dvhfplusr 31274 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( +g  `  (Scalar `  U ) )  =  O )
7249, 71syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( +g  `  (Scalar `  U ) )  =  O )
7372oveqd 5875 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( y ( +g  `  (Scalar `  U ) ) w )  =  ( y O w ) )
7473opeq2d 3803 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  <. ( x  o.  z ) ,  ( y ( +g  `  (Scalar `  U ) ) w ) >.  =  <. ( x  o.  z ) ,  ( y O w ) >. )
7569, 74eqtrd 2315 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( <. x ,  y >.  .+  <. z ,  w >. )  =  <. ( x  o.  z ) ,  ( y O w )
>. )
7675eqeq2d 2294 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( <. F ,  S >.  =  ( <.
x ,  y >.  .+  <. z ,  w >. )  <->  <. F ,  S >.  =  <. ( x  o.  z ) ,  ( y O w )
>. ) )
77 dihopelvalcp.f . . . . . . . . . 10  |-  F  e. 
_V
78 dihopelvalcp.s . . . . . . . . . 10  |-  S  e. 
_V
7977, 78opth 4245 . . . . . . . . 9  |-  ( <. F ,  S >.  = 
<. ( x  o.  z
) ,  ( y O w ) >.  <->  ( F  =  ( x  o.  z )  /\  S  =  ( y O w ) ) )
8062oveq2d 5874 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( y O w )  =  ( y O Z ) )
811, 6, 36, 37, 44, 70tendo0plr 30981 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  y  e.  E
)  ->  ( y O Z )  =  y )
8249, 51, 81syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( y O Z )  =  y )
8380, 82eqtrd 2315 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( y O w )  =  y )
8483eqeq2d 2294 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( S  =  ( y O w )  <->  S  =  y
) )
8584anbi2d 684 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( ( F  =  ( x  o.  z )  /\  S  =  ( y O w ) )  <->  ( F  =  ( x  o.  z )  /\  S  =  y ) ) )
8679, 85syl5bb 248 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( <. F ,  S >.  =  <. (
x  o.  z ) ,  ( y O w ) >.  <->  ( F  =  ( x  o.  z )  /\  S  =  y ) ) )
8776, 86bitrd 244 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) ) )  ->  ( <. F ,  S >.  =  ( <.
x ,  y >.  .+  <. z ,  w >. )  <->  ( F  =  ( x  o.  z
)  /\  S  =  y ) ) )
8887pm5.32da 622 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( (
( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  <. F ,  S >.  =  ( <. x ,  y
>.  .+  <. z ,  w >. ) )  <->  ( (
( x  =  ( y `  G )  /\  y  e.  E
)  /\  ( (
z  e.  T  /\  ( R `  z ) 
.<_  ( X  ./\  W
) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) ) )
89 simplll 734 . . . . . . . . . . 11  |-  ( ( ( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) )  ->  x  =  ( y `  G ) )
9089adantl 452 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  x  =  ( y `  G ) )
91 simprrr 741 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  S  =  y )
9291fveq1d 5527 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( S `  G
)  =  ( y `
 G ) )
9390, 92eqtr4d 2318 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  x  =  ( S `  G ) )
9491eqcomd 2288 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
y  =  S )
95 coass 5191 . . . . . . . . . . 11  |-  ( ( `' ( S `  G )  o.  ( S `  G )
)  o.  z )  =  ( `' ( S `  G )  o.  ( ( S `
 G )  o.  z ) )
96 simpl1 958 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
97 simpllr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) )  ->  y  e.  E )
9897adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
y  e.  E )
9991, 98eqeltrd 2357 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  S  e.  E )
10056adantrr 697 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  G  e.  T )
1016, 36, 37tendocl 30956 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  S  e.  E  /\  G  e.  T
)  ->  ( S `  G )  e.  T
)
10296, 99, 100, 101syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( S `  G
)  e.  T )
1031, 6, 36ltrn1o 30313 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S `  G )  e.  T
)  ->  ( S `  G ) : B -1-1-onto-> B
)
10496, 102, 103syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( S `  G
) : B -1-1-onto-> B )
105 f1ococnv1 5502 . . . . . . . . . . . . . 14  |-  ( ( S `  G ) : B -1-1-onto-> B  ->  ( `' ( S `  G )  o.  ( S `  G ) )  =  (  _I  |`  B ) )
106104, 105syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( `' ( S `
 G )  o.  ( S `  G
) )  =  (  _I  |`  B )
)
107106coeq1d 4845 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( ( `' ( S `  G )  o.  ( S `  G ) )  o.  z )  =  ( (  _I  |`  B )  o.  z ) )
10860ad2antrl 708 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
z  e.  T )
1091, 6, 36ltrn1o 30313 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  z  e.  T
)  ->  z : B
-1-1-onto-> B )
11096, 108, 109syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
z : B -1-1-onto-> B )
111 f1of 5472 . . . . . . . . . . . . 13  |-  ( z : B -1-1-onto-> B  ->  z : B
--> B )
112 fcoi2 5416 . . . . . . . . . . . . 13  |-  ( z : B --> B  -> 
( (  _I  |`  B )  o.  z )  =  z )
113110, 111, 1123syl 18 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( (  _I  |`  B )  o.  z )  =  z )
114107, 113eqtr2d 2316 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
z  =  ( ( `' ( S `  G )  o.  ( S `  G )
)  o.  z ) )
115 simprrl 740 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  F  =  ( x  o.  z ) )
11693coeq1d 4845 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( x  o.  z
)  =  ( ( S `  G )  o.  z ) )
117115, 116eqtrd 2315 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  F  =  ( ( S `  G )  o.  z ) )
118117coeq1d 4845 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( F  o.  `' ( S `  G ) )  =  ( ( ( S `  G
)  o.  z )  o.  `' ( S `
 G ) ) )
1196, 36ltrncnv 30335 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S `  G )  e.  T
)  ->  `' ( S `  G )  e.  T )
12096, 102, 119syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  `' ( S `  G )  e.  T
)
1216, 36ltrnco 30908 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( S `  G )  e.  T  /\  z  e.  T
)  ->  ( ( S `  G )  o.  z )  e.  T
)
12296, 102, 108, 121syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( ( S `  G )  o.  z
)  e.  T )
1236, 36ltrncom 30927 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  `' ( S `
 G )  e.  T  /\  ( ( S `  G )  o.  z )  e.  T )  ->  ( `' ( S `  G )  o.  (
( S `  G
)  o.  z ) )  =  ( ( ( S `  G
)  o.  z )  o.  `' ( S `
 G ) ) )
12496, 120, 122, 123syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( `' ( S `
 G )  o.  ( ( S `  G )  o.  z
) )  =  ( ( ( S `  G )  o.  z
)  o.  `' ( S `  G ) ) )
125118, 124eqtr4d 2318 . . . . . . . . . . 11  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( F  o.  `' ( S `  G ) )  =  ( `' ( S `  G
)  o.  ( ( S `  G )  o.  z ) ) )
12695, 114, 1253eqtr4a 2341 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
z  =  ( F  o.  `' ( S `
 G ) ) )
127 simplrr 737 . . . . . . . . . . 11  |-  ( ( ( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) )  ->  w  =  Z )
128127adantl 452 . . . . . . . . . 10  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  w  =  Z )
129126, 128jca 518 . . . . . . . . 9  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( z  =  ( F  o.  `' ( S `  G ) )  /\  w  =  Z ) )
13093, 94, 129jca31 520 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( ( x  =  ( y `
 G )  /\  y  e.  E )  /\  ( ( z  e.  T  /\  ( R `
 z )  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( ( x  =  ( S `  G
)  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )
131130ex 423 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( (
( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) )  ->  (
( x  =  ( S `  G )  /\  y  =  S )  /\  ( z  =  ( F  o.  `' ( S `  G ) )  /\  w  =  Z )
) ) )
132131pm4.71rd 616 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( (
( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) )  <->  ( (
( x  =  ( S `  G )  /\  y  =  S )  /\  ( z  =  ( F  o.  `' ( S `  G ) )  /\  w  =  Z )
)  /\  ( (
( x  =  ( y `  G )  /\  y  e.  E
)  /\  ( (
z  e.  T  /\  ( R `  z ) 
.<_  ( X  ./\  W
) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) ) ) )
13388, 132bitrd 244 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  (
( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X  ./\  W ) )  =  X ) )  ->  ( (
( ( x  =  ( y `  G
)  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  <. F ,  S >.  =  ( <. x ,  y
>.  .+  <. z ,  w >. ) )  <->  ( (
( x  =  ( S `  G )  /\  y  =  S )  /\  ( z  =  ( F  o.  `' ( S `  G ) )  /\  w  =  Z )
)  /\  ( (
( x  =  ( y `  G )  /\  y  e.  E
)  /\  ( (
z  e.  T  /\  ( R `  z ) 
.<_  ( X  ./\  W
) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) ) ) )
134 simprrl 740 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  F  =  ( x  o.  z ) )
135 simpll1 994 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
13689adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  x  =  ( y `  G ) )
13797adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
y  e.  E )
138135, 52syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( P  e.  A  /\  -.  P  .<_  W ) )
139 simpl3l 1010 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  -> 
( Q  e.  A  /\  -.  Q  .<_  W ) )
140139adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( Q  e.  A  /\  -.  Q  .<_  W ) )
141135, 138, 140, 55syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  G  e.  T )
142135, 137, 141, 57syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( y `  G
)  e.  T )
143136, 142eqeltrd 2357 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  x  e.  T )
14460ad2antrl 708 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
z  e.  T )
1456, 36ltrnco 30908 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  x  e.  T  /\  z  e.  T
)  ->  ( x  o.  z )  e.  T
)
146135, 143, 144, 145syl3anc 1182 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( x  o.  z
)  e.  T )
147134, 146eqeltrd 2357 . . . . . . . . 9  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  F  e.  T )
148 simpl1l 1006 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  ->  K  e.  HL )
149148adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  K  e.  HL )
150149, 20syl 15 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  K  e.  Lat )
1511, 6, 36, 43trlcl 30353 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  z  e.  T
)  ->  ( R `  z )  e.  B
)
152135, 144, 151syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( R `  z
)  e.  B )
153 simpl2l 1008 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  ->  X  e.  B )
154153adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  X  e.  B )
155 simpl1r 1007 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  ->  W  e.  H )
156155adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  W  e.  H )
157156, 24syl 15 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  ->  W  e.  B )
158150, 154, 157, 26syl3anc 1182 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( X  ./\  W
)  e.  B )
159 simprlr 739 . . . . . . . . . . 11  |-  ( ( ( x  =  ( y `  G )  /\  y  e.  E
)  /\  ( (
z  e.  T  /\  ( R `  z ) 
.<_  ( X  ./\  W
) )  /\  w  =  Z ) )  -> 
( R `  z
)  .<_  ( X  ./\  W ) )
160159ad2antrl 708 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( R `  z
)  .<_  ( X  ./\  W ) )
1611, 2, 4latmle1 14182 . . . . . . . . . . 11  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  W  e.  B )  ->  ( X  ./\  W
)  .<_  X )
162150, 154, 157, 161syl3anc 1182 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( X  ./\  W
)  .<_  X )
1631, 2, 150, 152, 158, 154, 160, 162lattrd 14164 . . . . . . . . 9  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( R `  z
)  .<_  X )
164147, 137, 163jca31 520 . . . . . . . 8  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( ( x  =  ( y `  G )  /\  y  e.  E )  /\  (
( z  e.  T  /\  ( R `  z
)  .<_  ( X  ./\  W ) )  /\  w  =  Z ) )  /\  ( F  =  (
x  o.  z )  /\  S  =  y ) ) )  -> 
( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )
165 simprll 738 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  ->  x  =  ( S `  G ) )
166165adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  ->  x  =  ( S `  G ) )
167 simprlr 739 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  -> 
y  =  S )
168167adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
y  =  S )
169168fveq1d 5527 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( y `  G
)  =  ( S `
 G ) )
170166, 169eqtr4d 2318 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  ->  x  =  ( y `  G ) )
171 simprlr 739 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
y  e.  E )
172170, 171jca 518 . . . . . . . . 9  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( x  =  ( y `  G )  /\  y  e.  E
) )
173 simprrl 740 . . . . . . . . . . . 12  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  -> 
z  =  ( F  o.  `' ( S `
 G ) ) )
174173adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
z  =  ( F  o.  `' ( S `
 G ) ) )
175 simpll1 994 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
176 simprll 738 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  ->  F  e.  T )
177168, 171eqeltrrd 2358 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  ->  S  e.  E )
178175, 52syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( P  e.  A  /\  -.  P  .<_  W ) )
179139adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( Q  e.  A  /\  -.  Q  .<_  W ) )
180175, 178, 179, 55syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  ->  G  e.  T )
181175, 177, 180, 101syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( S `  G
)  e.  T )
182175, 181, 119syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  ->  `' ( S `  G )  e.  T
)
1836, 36ltrnco 30908 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  `' ( S `  G )  e.  T
)  ->  ( F  o.  `' ( S `  G ) )  e.  T )
184175, 176, 182, 183syl3anc 1182 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( F  o.  `' ( S `  G ) )  e.  T )
185174, 184eqeltrd 2357 . . . . . . . . . 10  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
z  e.  T )
186 simprr 733 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( R `  z
)  .<_  X )
1872, 6, 36, 43trlle 30373 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  z  e.  T
)  ->  ( R `  z )  .<_  W )
188175, 185, 187syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  -.  X  .<_  W )  /\  ( ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( Q  .\/  ( X 
./\  W ) )  =  X ) )  /\  ( ( x  =  ( S `  G )  /\  y  =  S )  /\  (
z  =  ( F  o.  `' ( S `
 G ) )  /\  w  =  Z ) ) )  /\  ( ( F  e.  T  /\  y  e.  E )  /\  ( R `  z )  .<_  X ) )  -> 
( R `  z
)  .<_  W )
189<