Metamath Proof Explorer

Theorem dihopelvalcpre

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)

Ref Expression
Hypotheses 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 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 ) ) )

Proof

Step Hyp Ref Expression
1 dihopelvalcp.b 
 |-  B = ( Base ` K )
2 dihopelvalcp.l 
 |-  .<_ = ( le ` K )
3 dihopelvalcp.j 
 |-  .\/ = ( join ` K )
4 dihopelvalcp.m 
 |-  ./\ = ( meet ` K )
5 dihopelvalcp.a 
 |-  A = ( Atoms ` K )
6 dihopelvalcp.h 
 |-  H = ( LHyp ` K )
7 dihopelvalcp.p 
 |-  P = ( ( oc ` K ) ` W )
8 dihopelvalcp.t 
 |-  T = ( ( LTrn ` K ) ` W )
9 dihopelvalcp.r 
 |-  R = ( ( trL ` K ) ` W )
10 dihopelvalcp.e 
 |-  E = ( ( TEndo ` K ) ` W )
11 dihopelvalcp.i 
 |-  I = ( ( DIsoH ` K ) ` W )
12 dihopelvalcp.g 
 |-  G = ( iota_ g e. T ( g ` P ) = Q )
13 dihopelvalcp.f 
 |-  F e. _V
14 dihopelvalcp.s 
 |-  S e. _V
15 dihopelvalcp.z 
 |-  Z = ( h e. T |-> ( _I |` B ) )
16 dihopelvalcp.n 
 |-  N = ( ( DIsoB ` K ) ` W )
17 dihopelvalcp.c 
 |-  C = ( ( DIsoC ` K ) ` W )
18 dihopelvalcp.u 
 |-  U = ( ( DVecH ` K ) ` W )
19 dihopelvalcp.d 
 |-  .+ = ( +g ` U )
20 dihopelvalcp.v 
 |-  V = ( LSubSp ` U )
21 dihopelvalcp.y 
 |-  .(+) = ( LSSum ` U )
22 dihopelvalcp.o 
 |-  O = ( a e. E , b e. E |-> ( h e. T |-> ( ( a ` h ) o. ( b ` h ) ) ) )
23 1 2 3 4 5 6 11 16 17 18 21 dihvalcq 
 |-  ( ( ( 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 ) ) ) )
24 23 eleq2d 
 |-  ( ( ( 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 ) ) ) ) )
25 simp1 
 |-  ( ( ( 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 ) )
26 simp3l 
 |-  ( ( ( 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 ) )
27 2 5 6 18 17 20 diclss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( C ` Q ) e. V )
28 25 26 27 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( C ` Q ) e. V )
29 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> K e. HL )
30 29 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> K e. Lat )
31 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> X e. B )
32 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> W e. H )
33 1 6 lhpbase 
 |-  ( W e. H -> W e. B )
34 32 33 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> W e. B )
35 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
36 30 31 34 35 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( X ./\ W ) e. B )
37 1 2 4 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )
38 30 31 34 37 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( X ./\ W ) .<_ W )
39 1 2 6 18 16 20 diblss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( N ` ( X ./\ W ) ) e. V )
40 25 36 38 39 syl12anc 
 |-  ( ( ( 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 )
41 6 18 19 20 21 dvhopellsm 
 |-  ( ( ( 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 >. ) ) ) )
42 25 28 40 41 syl3anc 
 |-  ( ( ( 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 >. ) ) ) )
43 vex 
 |-  x e. _V
44 vex 
 |-  y e. _V
45 2 5 6 7 8 10 17 12 43 44 dicopelval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. x , y >. e. ( C ` Q ) <-> ( x = ( y ` G ) /\ y e. E ) ) )
46 25 26 45 syl2anc 
 |-  ( ( ( 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 ) ) )
47 1 2 6 8 9 15 16 dibopelval3 
 |-  ( ( ( 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 ) ) )
48 25 36 38 47 syl12anc 
 |-  ( ( ( 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 ) ) )
49 46 48 anbi12d 
 |-  ( ( ( 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 ) ) ) )
50 49 anbi1d 
 |-  ( ( ( 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 >. ) ) ) )
51 simpl1 
 |-  ( ( ( ( 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 ) )
52 simprll 
 |-  ( ( ( ( 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 ) )
53 simprlr 
 |-  ( ( ( ( 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 )
54 2 5 6 7 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
55 51 54 syl 
 |-  ( ( ( ( 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 ) )
56 simpl3l 
 |-  ( ( ( ( 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 ) )
57 2 5 6 8 12 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> G e. T )
58 51 55 56 57 syl3anc 
 |-  ( ( ( ( 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 )
59 6 8 10 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ y e. E /\ G e. T ) -> ( y ` G ) e. T )
60 51 53 58 59 syl3anc 
 |-  ( ( ( ( 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 )
61 52 60 eqeltrd 
 |-  ( ( ( ( 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 )
62 simprll 
 |-  ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) -> z e. T )
63 62 adantl 
 |-  ( ( ( ( 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 )
64 simprrr 
 |-  ( ( ( ( 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 )
65 1 6 8 10 15 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> Z e. E )
66 51 65 syl 
 |-  ( ( ( ( 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 )
67 64 66 eqeltrd 
 |-  ( ( ( ( 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 )
68 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
69 eqid 
 |-  ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
70 6 8 10 18 68 19 69 dvhopvadd 
 |-  ( ( ( 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 ) >. )
71 51 61 53 63 67 70 syl122anc 
 |-  ( ( ( ( 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 ) >. )
72 6 8 10 18 68 22 69 dvhfplusr 
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` ( Scalar ` U ) ) = O )
73 51 72 syl 
 |-  ( ( ( ( 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 )
74 73 oveqd 
 |-  ( ( ( ( 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 ) )
75 74 opeq2d 
 |-  ( ( ( ( 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 ) >. )
76 71 75 eqtrd 
 |-  ( ( ( ( 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 ) >. )
77 76 eqeq2d 
 |-  ( ( ( ( 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 ) >. ) )
78 13 14 opth 
 |-  ( <. F , S >. = <. ( x o. z ) , ( y O w ) >. <-> ( F = ( x o. z ) /\ S = ( y O w ) ) )
79 64 oveq2d 
 |-  ( ( ( ( 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 ) )
80 1 6 8 10 15 22 tendo0plr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ y e. E ) -> ( y O Z ) = y )
81 51 53 80 syl2anc 
 |-  ( ( ( ( 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 )
82 79 81 eqtrd 
 |-  ( ( ( ( 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 )
83 82 eqeq2d 
 |-  ( ( ( ( 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 ) )
84 83 anbi2d 
 |-  ( ( ( ( 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 ) ) )
85 78 84 syl5bb 
 |-  ( ( ( ( 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 ) ) )
86 77 85 bitrd 
 |-  ( ( ( ( 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 ) ) )
87 86 pm5.32da 
 |-  ( ( ( 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 ) ) ) )
88 simplll 
 |-  ( ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) /\ ( F = ( x o. z ) /\ S = y ) ) -> x = ( y ` G ) )
89 88 adantl 
 |-  ( ( ( ( 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 ) )
90 simprrr 
 |-  ( ( ( ( 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 )
91 90 fveq1d 
 |-  ( ( ( ( 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 ) )
92 89 91 eqtr4d 
 |-  ( ( ( ( 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 ) )
93 90 eqcomd 
 |-  ( ( ( ( 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 )
94 coass 
 |-  ( ( `' ( S ` G ) o. ( S ` G ) ) o. z ) = ( `' ( S ` G ) o. ( ( S ` G ) o. z ) )
95 simpl1 
 |-  ( ( ( ( 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 ) )
96 simpllr 
 |-  ( ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) /\ ( F = ( x o. z ) /\ S = y ) ) -> y e. E )
97 96 adantl 
 |-  ( ( ( ( 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 )
98 90 97 eqeltrd 
 |-  ( ( ( ( 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 )
99 58 adantrr 
 |-  ( ( ( ( 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 )
100 6 8 10 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ G e. T ) -> ( S ` G ) e. T )
101 95 98 99 100 syl3anc 
 |-  ( ( ( ( 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 )
102 1 6 8 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` G ) e. T ) -> ( S ` G ) : B -1-1-onto-> B )
103 95 101 102 syl2anc 
 |-  ( ( ( ( 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 )
104 f1ococnv1 
 |-  ( ( S ` G ) : B -1-1-onto-> B -> ( `' ( S ` G ) o. ( S ` G ) ) = ( _I |` B ) )
105 103 104 syl 
 |-  ( ( ( ( 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 ) )
106 105 coeq1d 
 |-  ( ( ( ( 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 ) )
107 62 ad2antrl 
 |-  ( ( ( ( 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 )
108 1 6 8 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ z e. T ) -> z : B -1-1-onto-> B )
109 95 107 108 syl2anc 
 |-  ( ( ( ( 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 )
110 f1of 
 |-  ( z : B -1-1-onto-> B -> z : B --> B )
111 fcoi2 
 |-  ( z : B --> B -> ( ( _I |` B ) o. z ) = z )
112 109 110 111 3syl 
 |-  ( ( ( ( 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 )
113 106 112 eqtr2d 
 |-  ( ( ( ( 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 ) )
114 simprrl 
 |-  ( ( ( ( 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 ) )
115 92 coeq1d 
 |-  ( ( ( ( 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 ) )
116 114 115 eqtrd 
 |-  ( ( ( ( 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 ) )
117 116 coeq1d 
 |-  ( ( ( ( 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 ) ) )
118 6 8 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` G ) e. T ) -> `' ( S ` G ) e. T )
119 95 101 118 syl2anc 
 |-  ( ( ( ( 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 )
120 6 8 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` G ) e. T /\ z e. T ) -> ( ( S ` G ) o. z ) e. T )
121 95 101 107 120 syl3anc 
 |-  ( ( ( ( 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 )
122 6 8 ltrncom 
 |-  ( ( ( 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 ) ) )
123 95 119 121 122 syl3anc 
 |-  ( ( ( ( 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 ) ) )
124 117 123 eqtr4d 
 |-  ( ( ( ( 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 ) ) )
125 94 113 124 3eqtr4a 
 |-  ( ( ( ( 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 ) ) )
126 simplrr 
 |-  ( ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) /\ ( F = ( x o. z ) /\ S = y ) ) -> w = Z )
127 126 adantl 
 |-  ( ( ( ( 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 )
128 125 127 jca 
 |-  ( ( ( ( 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 ) )
129 92 93 128 jca31 
 |-  ( ( ( ( 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 ) ) )
130 129 ex 
 |-  ( ( ( 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 ) ) ) )
131 130 pm4.71rd 
 |-  ( ( ( 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 ) ) ) ) )
132 87 131 bitrd 
 |-  ( ( ( 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 ) ) ) ) )
133 simprrl 
 |-  ( ( ( ( ( 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 ) )
134 simpll1 
 |-  ( ( ( ( ( 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 ) )
135 88 adantl 
 |-  ( ( ( ( ( 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 ) )
136 96 adantl 
 |-  ( ( ( ( ( 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 )
137 134 54 syl 
 |-  ( ( ( ( ( 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 ) )
138 simpl3l 
 |-  ( ( ( ( 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 ) )
139 138 adantr 
 |-  ( ( ( ( ( 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 ) )
140 134 137 139 57 syl3anc 
 |-  ( ( ( ( ( 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 )
141 134 136 140 59 syl3anc 
 |-  ( ( ( ( ( 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 )
142 135 141 eqeltrd 
 |-  ( ( ( ( ( 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 )
143 62 ad2antrl 
 |-  ( ( ( ( ( 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 )
144 6 8 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T /\ z e. T ) -> ( x o. z ) e. T )
145 134 142 143 144 syl3anc 
 |-  ( ( ( ( ( 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 )
146 133 145 eqeltrd 
 |-  ( ( ( ( ( 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 )
147 simpl1l 
 |-  ( ( ( ( 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 )
148 147 adantr 
 |-  ( ( ( ( ( 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 )
149 148 hllatd 
 |-  ( ( ( ( ( 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 )
150 1 6 8 9 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ z e. T ) -> ( R ` z ) e. B )
151 134 143 150 syl2anc 
 |-  ( ( ( ( ( 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 )
152 simpl2l 
 |-  ( ( ( ( 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 )
153 152 adantr 
 |-  ( ( ( ( ( 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 )
154 simpl1r 
 |-  ( ( ( ( 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 )
155 154 adantr 
 |-  ( ( ( ( ( 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 )
156 155 33 syl 
 |-  ( ( ( ( ( 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 )
157 149 153 156 35 syl3anc 
 |-  ( ( ( ( ( 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 )
158 simprlr 
 |-  ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) -> ( R ` z ) .<_ ( X ./\ W ) )
159 158 ad2antrl 
 |-  ( ( ( ( ( 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 ) )
160 1 2 4 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ X )
161 149 153 156 160 syl3anc 
 |-  ( ( ( ( ( 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 )
162 1 2 149 151 157 153 159 161 lattrd 
 |-  ( ( ( ( ( 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 )
163 146 136 162 jca31 
 |-  ( ( ( ( ( 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 ) )
164 simprll 
 |-  ( ( ( ( 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 ) )
165 164 adantr 
 |-  ( ( ( ( ( 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 ) )
166 simprlr 
 |-  ( ( ( ( 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 )
167 166 adantr 
 |-  ( ( ( ( ( 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 )
168 167 fveq1d 
 |-  ( ( ( ( ( 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 ) )
169 165 168 eqtr4d 
 |-  ( ( ( ( ( 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 ) )
170 simprlr 
 |-  ( ( ( ( ( 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 )
171 169 170 jca 
 |-  ( ( ( ( ( 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 ) )
172 simprrl 
 |-  ( ( ( ( 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 ) ) )
173 172 adantr 
 |-  ( ( ( ( ( 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 ) ) )
174 simpll1 
 |-  ( ( ( ( ( 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 ) )
175 simprll 
 |-  ( ( ( ( ( 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 )
176 167 170 eqeltrrd 
 |-  ( ( ( ( ( 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 )
177 174 54 syl 
 |-  ( ( ( ( ( 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 ) )
178 138 adantr 
 |-  ( ( ( ( ( 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 ) )
179 174 177 178 57 syl3anc 
 |-  ( ( ( ( ( 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 )
180 174 176 179 100 syl3anc 
 |-  ( ( ( ( ( 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 )
181 174 180 118 syl2anc 
 |-  ( ( ( ( ( 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 )
182 6 8 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ `' ( S ` G ) e. T ) -> ( F o. `' ( S ` G ) ) e. T )
183 174 175 181 182 syl3anc 
 |-  ( ( ( ( ( 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 )
184 173 183 eqeltrd 
 |-  ( ( ( ( ( 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 )
185 simprr 
 |-  ( ( ( ( ( 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 )
186 2 6 8 9 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ z e. T ) -> ( R ` z ) .<_ W )
187 174 184 186 syl2anc 
 |-  ( ( ( ( ( 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 )
188 147 adantr 
 |-  ( ( ( ( ( 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 )
189 188 hllatd 
 |-  ( ( ( ( ( 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. Lat )
190 174 184 150 syl2anc 
 |-  ( ( ( ( ( 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 ) e. B )
191 152 adantr 
 |-  ( ( ( ( ( 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 e. B )
192 154 adantr 
 |-  ( ( ( ( ( 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 ) ) -> W e. H )
193 192 33 syl 
 |-  ( ( ( ( ( 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 ) ) -> W e. B )
194 1 2 4 latlem12 
 |-  ( ( K e. Lat /\ ( ( R ` z ) e. B /\ X e. B /\ W e. B ) ) -> ( ( ( R ` z ) .<_ X /\ ( R ` z ) .<_ W ) <-> ( R ` z ) .<_ ( X ./\ W ) ) )
195 189 190 191 193 194 syl13anc 
 |-  ( ( ( ( ( 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 /\ ( R ` z ) .<_ W ) <-> ( R ` z ) .<_ ( X ./\ W ) ) )
196 185 187 195 mpbi2and 
 |-  ( ( ( ( ( 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 ./\ W ) )
197 simprrr 
 |-  ( ( ( ( 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 = Z )
198 197 adantr 
 |-  ( ( ( ( ( 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 ) ) -> w = Z )
199 184 196 198 jca31 
 |-  ( ( ( ( ( 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 /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) )
200 174 180 102 syl2anc 
 |-  ( ( ( ( ( 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 ) : B -1-1-onto-> B )
201 200 104 syl 
 |-  ( ( ( ( ( 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 ) o. ( S ` G ) ) = ( _I |` B ) )
202 201 coeq2d 
 |-  ( ( ( ( ( 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 ) o. ( S ` G ) ) ) = ( F o. ( _I |` B ) ) )
203 1 6 8 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : B -1-1-onto-> B )
204 174 175 203 syl2anc 
 |-  ( ( ( ( ( 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 : B -1-1-onto-> B )
205 f1of 
 |-  ( F : B -1-1-onto-> B -> F : B --> B )
206 fcoi1 
 |-  ( F : B --> B -> ( F o. ( _I |` B ) ) = F )
207 204 205 206 3syl 
 |-  ( ( ( ( ( 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. ( _I |` B ) ) = F )
208 202 207 eqtr2d 
 |-  ( ( ( ( ( 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 = ( F o. ( `' ( S ` G ) o. ( S ` G ) ) ) )
209 coass 
 |-  ( ( F o. `' ( S ` G ) ) o. ( S ` G ) ) = ( F o. ( `' ( S ` G ) o. ( S ` G ) ) )
210 208 209 eqtr4di 
 |-  ( ( ( ( ( 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 = ( ( F o. `' ( S ` G ) ) o. ( S ` G ) ) )
211 6 8 ltrncom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` G ) e. T /\ ( F o. `' ( S ` G ) ) e. T ) -> ( ( S ` G ) o. ( F o. `' ( S ` G ) ) ) = ( ( F o. `' ( S ` G ) ) o. ( S ` G ) ) )
212 174 180 183 211 syl3anc 
 |-  ( ( ( ( ( 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 ) o. ( F o. `' ( S ` G ) ) ) = ( ( F o. `' ( S ` G ) ) o. ( S ` G ) ) )
213 210 212 eqtr4d 
 |-  ( ( ( ( ( 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 = ( ( S ` G ) o. ( F o. `' ( S ` G ) ) ) )
214 165 173 coeq12d 
 |-  ( ( ( ( ( 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 o. z ) = ( ( S ` G ) o. ( F o. `' ( S ` G ) ) ) )
215 213 214 eqtr4d 
 |-  ( ( ( ( ( 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 = ( x o. z ) )
216 167 eqcomd 
 |-  ( ( ( ( ( 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 = y )
217 215 216 jca 
 |-  ( ( ( ( ( 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 = ( x o. z ) /\ S = y ) )
218 171 199 217 jca31 
 |-  ( ( ( ( ( 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 ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) /\ ( F = ( x o. z ) /\ S = y ) ) )
219 163 218 impbida 
 |-  ( ( ( ( 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 ) ) )
220 219 pm5.32da 
 |-  ( ( ( 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 = ( S ` G ) /\ y = S ) /\ ( z = ( F o. `' ( S ` G ) ) /\ w = Z ) ) /\ ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) ) )
221 df-3an 
 |-  ( ( ( x = ( S ` G ) /\ y = S ) /\ ( z = ( F o. `' ( S ` G ) ) /\ w = Z ) /\ ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) <-> ( ( ( x = ( S ` G ) /\ y = S ) /\ ( z = ( F o. `' ( S ` G ) ) /\ w = Z ) ) /\ ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) )
222 220 221 bitr4di 
 |-  ( ( ( 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 = ( S ` G ) /\ y = S ) /\ ( z = ( F o. `' ( S ` G ) ) /\ w = Z ) /\ ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) ) )
223 50 132 222 3bitrd 
 |-  ( ( ( 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 = ( S ` G ) /\ y = S ) /\ ( z = ( F o. `' ( S ` G ) ) /\ w = Z ) /\ ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) ) )
224 223 4exbidv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( 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 >. ) ) <-> E. x E. y E. z E. w ( ( x = ( S ` G ) /\ y = S ) /\ ( z = ( F o. `' ( S ` G ) ) /\ w = Z ) /\ ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) ) )
225 fvex 
 |-  ( S ` G ) e. _V
226 225 cnvex 
 |-  `' ( S ` G ) e. _V
227 13 226 coex 
 |-  ( F o. `' ( S ` G ) ) e. _V
228 8 fvexi 
 |-  T e. _V
229 228 mptex 
 |-  ( h e. T |-> ( _I |` B ) ) e. _V
230 15 229 eqeltri 
 |-  Z e. _V
231 biidd 
 |-  ( x = ( S ` G ) -> ( ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) <-> ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) )
232 eleq1 
 |-  ( y = S -> ( y e. E <-> S e. E ) )
233 232 anbi2d 
 |-  ( y = S -> ( ( F e. T /\ y e. E ) <-> ( F e. T /\ S e. E ) ) )
234 233 anbi1d 
 |-  ( y = S -> ( ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) <-> ( ( F e. T /\ S e. E ) /\ ( R ` z ) .<_ X ) ) )
235 fveq2 
 |-  ( z = ( F o. `' ( S ` G ) ) -> ( R ` z ) = ( R ` ( F o. `' ( S ` G ) ) ) )
236 235 breq1d 
 |-  ( z = ( F o. `' ( S ` G ) ) -> ( ( R ` z ) .<_ X <-> ( R ` ( F o. `' ( S ` G ) ) ) .<_ X ) )
237 236 anbi2d 
 |-  ( z = ( F o. `' ( S ` G ) ) -> ( ( ( F e. T /\ S e. E ) /\ ( R ` z ) .<_ X ) <-> ( ( F e. T /\ S e. E ) /\ ( R ` ( F o. `' ( S ` G ) ) ) .<_ X ) ) )
238 biidd 
 |-  ( w = Z -> ( ( ( F e. T /\ S e. E ) /\ ( R ` ( F o. `' ( S ` G ) ) ) .<_ X ) <-> ( ( F e. T /\ S e. E ) /\ ( R ` ( F o. `' ( S ` G ) ) ) .<_ X ) ) )
239 225 14 227 230 231 234 237 238 ceqsex4v 
 |-  ( E. x E. y E. z E. w ( ( x = ( S ` G ) /\ y = S ) /\ ( z = ( F o. `' ( S ` G ) ) /\ w = Z ) /\ ( ( F e. T /\ y e. E ) /\ ( R ` z ) .<_ X ) ) <-> ( ( F e. T /\ S e. E ) /\ ( R ` ( F o. `' ( S ` G ) ) ) .<_ X ) )
240 224 239 bitrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( 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 >. ) ) <-> ( ( F e. T /\ S e. E ) /\ ( R ` ( F o. `' ( S ` G ) ) ) .<_ X ) ) )
241 24 42 240 3bitrd 
 |-  ( ( ( 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 ) ) )