Theorem dihopelvalcpre 34887

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.

Step	Hyp	Ref	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 )
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	dihvalcq 34875	. . 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 ) ) ) )
13	12	eleq2d 2534	. 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 1030	. . 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 1058	. . . 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 )
17	2, 5, 6, 10, 9, 16	diclss 34832	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( C ` Q ) e. V )
18	14, 15, 17	syl2anc 673	. . 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 1054	. . . . . 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 33000	. . . . . 6 |- ( K e. HL -> K e. Lat )
21	19, 20	syl 17	. . . . 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 1056	. . . . 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 1055	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> W e. H )
24	1, 6	lhpbase 33634	. . . . . 6 |- ( W e. H -> W e. B )
25	23, 24	syl 17	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> W e. B )
26	1, 4	latmcl 16376	. . . . 5 |- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
27	21, 22, 25, 26	syl3anc 1292	. . . 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 )
28	1, 2, 4	latmle2 16401	. . . . 5 |- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )
29	21, 22, 25, 28	syl3anc 1292	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( Q e. A /\ -. Q .<_ W ) /\ ( Q .\/ ( X ./\ W ) ) = X ) ) -> ( X ./\ W ) .<_ W )
30	1, 2, 6, 10, 8, 16	diblss 34809	. . . 4 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( N ` ( X ./\ W ) ) e. V )
31	14, 27, 29, 30	syl12anc 1290	. . 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 )
33	6, 10, 32, 16, 11	dvhopellsm 34756	. . 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 >. ) ) ) )
34	14, 18, 31, 33	syl3anc 1292	. 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 3034	. . . . . . . . 9 |- x e. _V
40		vex 3034	. . . . . . . . 9 |- y e. _V
41	2, 5, 6, 35, 36, 37, 9, 38, 39, 40	dicopelval2 34820	. . . . . . . 8 |- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. x , y >. e. ( C ` Q ) <-> ( x = ( y ` G ) /\ y e. E ) ) )
42	14, 15, 41	syl2anc 673	. . . . . . 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 ) )
45	1, 2, 6, 36, 43, 44, 8	dibopelval3 34787	. . . . . . . 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 ) ) )
46	14, 27, 29, 45	syl12anc 1290	. . . . . . 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 ) ) )
47	42, 46	anbi12d 725	. . . . . 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 ) ) ) )
48	47	anbi1d 719	. . . . 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 1033	. . . . . . . . . . 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 780	. . . . . . . . . . . 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 781	. . . . . . . . . . . . 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 )
52	2, 5, 6, 35	lhpocnel2 33655	. . . . . . . . . . . . . . 15 |- ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
53	49, 52	syl 17	. . . . . . . . . . . . . 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 1085	. . . . . . . . . . . . . 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 ) )
55	2, 5, 6, 36, 38	ltrniotacl 34217	. . . . . . . . . . . . . 14 |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> G e. T )
56	49, 53, 54, 55	syl3anc 1292	. . . . . . . . . . . . 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 )
57	6, 36, 37	tendocl 34405	. . . . . . . . . . . . 13 |- ( ( ( K e. HL /\ W e. H ) /\ y e. E /\ G e. T ) -> ( y ` G ) e. T )
58	49, 51, 56, 57	syl3anc 1292	. . . . . . . . . . . 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 )
59	50, 58	eqeltrd 2549	. . . . . . . . . . 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 780	. . . . . . . . . . . 12 |- ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) -> z e. T )
61	60	adantl 473	. . . . . . . . . . 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 783	. . . . . . . . . . . 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 )
63	1, 6, 36, 37, 44	tendo0cl 34428	. . . . . . . . . . . . 13 |- ( ( K e. HL /\ W e. H ) -> Z e. E )
64	49, 63	syl 17	. . . . . . . . . . . 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 )
65	62, 64	eqeltrd 2549	. . . . . . . . . . 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 2471	. . . . . . . . . . . 12 |- (Scalar ` U ) = (Scalar ` U )
67		eqid 2471	. . . . . . . . . . . 12 |- ( +g ` (Scalar ` U ) ) = ( +g ` (Scalar ` U ) )
68	6, 36, 37, 10, 66, 32, 67	dvhopvadd 34732	. . . . . . . . . . 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 ) >. )
69	49, 59, 51, 61, 65, 68	syl122anc 1301	. . . . . . . . . 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 ) ) ) )
71	6, 36, 37, 10, 66, 70, 67	dvhfplusr 34723	. . . . . . . . . . . . 13 |- ( ( K e. HL /\ W e. H ) -> ( +g ` (Scalar ` U ) ) = O )
72	49, 71	syl 17	. . . . . . . . . . . 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 )
73	72	oveqd 6325	. . . . . . . . . . 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 ) )
74	73	opeq2d 4165	. . . . . . . . . 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 ) >. )
75	69, 74	eqtrd 2505	. . . . . . . . 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 ) >. )
76	75	eqeq2d 2481	. . . . . . . 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
79	77, 78	opth 4676	. . . . . . . . 9 |- ( <. F , S >. = <. ( x o. z ) , ( y O w ) >. <-> ( F = ( x o. z ) /\ S = ( y O w ) ) )
80	62	oveq2d 6324	. . . . . . . . . . . 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 ) )
81	1, 6, 36, 37, 44, 70	tendo0plr 34430	. . . . . . . . . . . . 13 |- ( ( ( K e. HL /\ W e. H ) /\ y e. E ) -> ( y O Z ) = y )
82	49, 51, 81	syl2anc 673	. . . . . . . . . . . 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 )
83	80, 82	eqtrd 2505	. . . . . . . . . . 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 )
84	83	eqeq2d 2481	. . . . . . . . . 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 ) )
85	84	anbi2d 718	. . . . . . . . 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 ) ) )
86	79, 85	syl5bb 265	. . . . . . . 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 ) ) )
87	76, 86	bitrd 261	. . . . . . 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 ) ) )
88	87	pm5.32da 653	. . . . . 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 776	. . . . . . . . . . 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 ) )
90	89	adantl 473	. . . . . . . . . 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 783	. . . . . . . . . . 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 )
92	91	fveq1d 5881	. . . . . . . . . 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 ) )
93	90, 92	eqtr4d 2508	. . . . . . . . 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 ) )
94	91	eqcomd 2477	. . . . . . . . 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 5361	. . . . . . . . . . 11 |- ( ( `' ( S ` G ) o. ( S ` G ) ) o. z ) = ( `' ( S ` G ) o. ( ( S ` G ) o. z ) )
96		simpl1 1033	. . . . . . . . . . . . . . 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 777	. . . . . . . . . . . . . . . . . 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 )
98	97	adantl 473	. . . . . . . . . . . . . . . . 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 )
99	91, 98	eqeltrd 2549	. . . . . . . . . . . . . . . 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 )
100	56	adantrr 731	. . . . . . . . . . . . . . . 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 )
101	6, 36, 37	tendocl 34405	. . . . . . . . . . . . . . . 16 |- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ G e. T ) -> ( S ` G ) e. T )
102	96, 99, 100, 101	syl3anc 1292	. . . . . . . . . . . . . . 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 )
103	1, 6, 36	ltrn1o 33760	. . . . . . . . . . . . . . 15 |- ( ( ( K e. HL /\ W e. H ) /\ ( S ` G ) e. T ) -> ( S ` G ) : B -1-1-onto-> B )
104	96, 102, 103	syl2anc 673	. . . . . . . . . . . . . 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 5856	. . . . . . . . . . . . . 14 |- ( ( S ` G ) : B -1-1-onto-> B -> ( `' ( S ` G ) o. ( S ` G ) ) = ( _I |` B ) )
106	104, 105	syl 17	. . . . . . . . . . . . 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 ) )
107	106	coeq1d 5001	. . . . . . . . . . . 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 ) )
108	60	ad2antrl 742	. . . . . . . . . . . . . 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 )
109	1, 6, 36	ltrn1o 33760	. . . . . . . . . . . . . 14 |- ( ( ( K e. HL /\ W e. H ) /\ z e. T ) -> z : B -1-1-onto-> B )
110	96, 108, 109	syl2anc 673	. . . . . . . . . . . . 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 5828	. . . . . . . . . . . . 13 |- ( z : B -1-1-onto-> B -> z : B --> B )
112		fcoi2 5770	. . . . . . . . . . . . 13 |- ( z : B --> B -> ( ( _I |` B ) o. z ) = z )
113	110, 111, 112	3syl 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 )
114	107, 113	eqtr2d 2506	. . . . . . . . . . 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 782	. . . . . . . . . . . . . 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 ) )
116	93	coeq1d 5001	. . . . . . . . . . . . . 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 ) )
117	115, 116	eqtrd 2505	. . . . . . . . . . . . 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 ) )
118	117	coeq1d 5001	. . . . . . . . . . . 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 ) ) )
119	6, 36	ltrncnv 33782	. . . . . . . . . . . . . 14 |- ( ( ( K e. HL /\ W e. H ) /\ ( S ` G ) e. T ) -> `' ( S ` G ) e. T )
120	96, 102, 119	syl2anc 673	. . . . . . . . . . . . 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 )
121	6, 36	ltrnco 34357	. . . . . . . . . . . . . 14 |- ( ( ( K e. HL /\ W e. H ) /\ ( S ` G ) e. T /\ z e. T ) -> ( ( S ` G ) o. z ) e. T )
122	96, 102, 108, 121	syl3anc 1292	. . . . . . . . . . . . 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 )
123	6, 36	ltrncom 34376	. . . . . . . . . . . . 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 ) ) )
124	96, 120, 122, 123	syl3anc 1292	. . . . . . . . . . . 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 ) ) )
125	118, 124	eqtr4d 2508	. . . . . . . . . . 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 ) ) )
126	95, 114, 125	3eqtr4a 2531	. . . . . . . . . 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 779	. . . . . . . . . . 11 |- ( ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) /\ ( F = ( x o. z ) /\ S = y ) ) -> w = Z )
128	127	adantl 473	. . . . . . . . . 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 )
129	126, 128	jca 541	. . . . . . . . 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 ) )
130	93, 94, 129	jca31 543	. . . . . . . 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 ) ) )
131	130	ex 441	. . . . . . 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 ) ) ) )
132	131	pm4.71rd 647	. . . . . 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 ) ) ) ) )
133	88, 132	bitrd 261	. . . . 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 782	. . . . . . . . . 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 1069	. . . . . . . . . . 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 ) )
136	89	adantl 473	. . . . . . . . . . . 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 ) )
137	97	adantl 473	. . . . . . . . . . . . 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 )
138	135, 52	syl 17	. . . . . . . . . . . . . 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 1085	. . . . . . . . . . . . . . 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 ) )
140	139	adantr 472	. . . . . . . . . . . . . 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 ) )
141	135, 138, 140, 55	syl3anc 1292	. . . . . . . . . . . . 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 )
142	135, 137, 141, 57	syl3anc 1292	. . . . . . . . . . . 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 )
143	136, 142	eqeltrd 2549	. . . . . . . . . . 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 )
144	60	ad2antrl 742	. . . . . . . . . . 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 )
145	6, 36	ltrnco 34357	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ W e. H ) /\ x e. T /\ z e. T ) -> ( x o. z ) e. T )
146	135, 143, 144, 145	syl3anc 1292	. . . . . . . . . 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 )
147	134, 146	eqeltrd 2549	. . . . . . . . 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 1081	. . . . . . . . . . . 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 )
149	148	adantr 472	. . . . . . . . . . 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 )
150	149, 20	syl 17	. . . . . . . . . 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 )
151	1, 6, 36, 43	trlcl 33801	. . . . . . . . . . 11 |- ( ( ( K e. HL /\ W e. H ) /\ z e. T ) -> ( R ` z ) e. B )
152	135, 144, 151	syl2anc 673	. . . . . . . . . 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 1083	. . . . . . . . . . . 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 )
154	153	adantr 472	. . . . . . . . . . 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 1082	. . . . . . . . . . . . 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 )
156	155	adantr 472	. . . . . . . . . . . 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 )
157	156, 24	syl 17	. . . . . . . . . . 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 )
158	150, 154, 157, 26	syl3anc 1292	. . . . . . . . . 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 781	. . . . . . . . . . 11 |- ( ( ( x = ( y ` G ) /\ y e. E ) /\ ( ( z e. T /\ ( R ` z ) .<_ ( X ./\ W ) ) /\ w = Z ) ) -> ( R ` z ) .<_ ( X ./\ W ) )
160	159	ad2antrl 742	. . . . . . . . . 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 ) )
161	1, 2, 4	latmle1 16400	. . . . . . . . . . 11 |- ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ X )
162	150, 154, 157, 161	syl3anc 1292	. . . . . . . . . 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 )
163	1, 2, 150, 152, 158, 154, 160, 162	lattrd 16382	. . . . . . . . 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 )
164	147, 137, 163	jca31 543	. . . . . . . 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 780	. . . . . . . . . . . 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 ) )
166	165	adantr 472	. . . . . . . . . . 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 781	. . . . . . . . . . . . 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 )
168	167	adantr 472	. . . . . . . . . . . 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 )
169	168	fveq1d 5881	. . . . . . . . . . 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 ) )
170	166, 169	eqtr4d 2508	. . . . . . . . . 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 781	. . . . . . . . . 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 )
172	170, 171	jca 541	. . . . . . . . 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 782	. . . . . . . . . . . 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 ) ) )
174	173	adantr 472	. . . . . . . . . . 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 1069	. . . . . . . . . . . 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 780	. . . . . . . . . . . 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 )
177	168, 171	eqeltrrd 2550	. . . . . . . . . . . . . 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 )
178	175, 52	syl 17	. . . . . . . . . . . . . . 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 ) )
179	139	adantr 472	. . . . . . . . . . . . . . 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 ) )
180	175, 178, 179, 55	syl3anc 1292	. . . . . . . . . . . . . 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 )
181	175, 177, 180, 101	syl3anc 1292	. . . . . . . . . . . . 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 )
182	175, 181, 119	syl2anc 673	. . . . . . . . . . . 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 )
183	6, 36	ltrnco 34357	. . . . . . . . . . . 12 |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ `' ( S ` G ) e. T ) -> ( F o. `' ( S ` G ) ) e. T )
184	175, 176, 182, 183	syl3anc 1292	. . . . . . . . . . 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 )
185	174, 184	eqeltrd 2549	. . . . . . . . . 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 774	. . . . . . . . . . 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 )
187	2, 6, 36, 43	trlle 33821	. . . . . . . . . . . 12 |- ( ( ( K e. HL /\ W e. H ) /\ z e. T ) -> ( R ` z ) .<_ W )
188	175, 185, 187	syl2anc 673	. . . . . . . . . . 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	148	adantr 472	. . . . . . . . . . . . 13 |- ( ( ( ( ( K e. HL /\ W e.