# 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 )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 syl6bbr
` |-  ( ( ( 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 syl6bb
` |-  ( ( ( 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 ) ) )`