Metamath Proof Explorer

Theorem dih1dimatlem0

Description: Lemma for dih1dimat . (Contributed by NM, 11-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h 
|- H = ( LHyp ` K )
dih1dimat.u 
|- U = ( ( DVecH ` K ) ` W )
dih1dimat.i 
|- I = ( ( DIsoH ` K ) ` W )
dih1dimat.a 
|- A = ( LSAtoms ` U )
dih1dimat.b 
|- B = ( Base ` K )
dih1dimat.l 
|- .<_ = ( le ` K )
dih1dimat.c 
|- C = ( Atoms ` K )
dih1dimat.p 
|- P = ( ( oc ` K ) ` W )
dih1dimat.t 
|- T = ( ( LTrn ` K ) ` W )
dih1dimat.r 
|- R = ( ( trL ` K ) ` W )
dih1dimat.e 
|- E = ( ( TEndo ` K ) ` W )
dih1dimat.o 
|- O = ( h e. T |-> ( _I |` B ) )
dih1dimat.d 
|- F = ( Scalar ` U )
dih1dimat.j 
|- J = ( invr ` F )
dih1dimat.v 
|- V = ( Base ` U )
dih1dimat.m 
|- .x. = ( .s ` U )
dih1dimat.s 
|- S = ( LSubSp ` U )
dih1dimat.n 
|- N = ( LSpan ` U )
dih1dimat.z 
|- .0. = ( 0g ` U )
dih1dimat.g 
|- G = ( iota_ h e. T ( h ` P ) = ( ( ( J ` s ) ` f ) ` P ) )
Assertion dih1dimatlem0 
|- ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( ( i = ( p ` G ) /\ p e. E ) <-> ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dih1dimat.h 
 |-  H = ( LHyp ` K )
2 dih1dimat.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dih1dimat.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dih1dimat.a 
 |-  A = ( LSAtoms ` U )
5 dih1dimat.b 
 |-  B = ( Base ` K )
6 dih1dimat.l 
 |-  .<_ = ( le ` K )
7 dih1dimat.c 
 |-  C = ( Atoms ` K )
8 dih1dimat.p 
 |-  P = ( ( oc ` K ) ` W )
9 dih1dimat.t 
 |-  T = ( ( LTrn ` K ) ` W )
10 dih1dimat.r 
 |-  R = ( ( trL ` K ) ` W )
11 dih1dimat.e 
 |-  E = ( ( TEndo ` K ) ` W )
12 dih1dimat.o 
 |-  O = ( h e. T |-> ( _I |` B ) )
13 dih1dimat.d 
 |-  F = ( Scalar ` U )
14 dih1dimat.j 
 |-  J = ( invr ` F )
15 dih1dimat.v 
 |-  V = ( Base ` U )
16 dih1dimat.m 
 |-  .x. = ( .s ` U )
17 dih1dimat.s 
 |-  S = ( LSubSp ` U )
18 dih1dimat.n 
 |-  N = ( LSpan ` U )
19 dih1dimat.z 
 |-  .0. = ( 0g ` U )
20 dih1dimat.g 
 |-  G = ( iota_ h e. T ( h ` P ) = ( ( ( J ` s ) ` f ) ` P ) )
21 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> i = ( p ` G ) )
22 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( K e. HL /\ W e. H ) )
23 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> p e. E )
24 6 7 1 8 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. C /\ -. P .<_ W ) )
25 22 24 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( P e. C /\ -. P .<_ W ) )
26 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> s e. E )
27 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> s =/= O )
28 5 1 9 11 12 2 13 14 tendoinvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ s =/= O ) -> ( ( J ` s ) e. E /\ ( J ` s ) =/= O ) )
29 28 simpld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ s =/= O ) -> ( J ` s ) e. E )
30 22 26 27 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( J ` s ) e. E )
31 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> f e. T )
32 1 9 11 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( J ` s ) e. E /\ f e. T ) -> ( ( J ` s ) ` f ) e. T )
33 22 30 31 32 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( ( J ` s ) ` f ) e. T )
34 6 7 1 9 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( J ` s ) ` f ) e. T /\ ( P e. C /\ -. P .<_ W ) ) -> ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) )
35 22 33 25 34 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) )
36 6 7 1 9 20 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. C /\ -. P .<_ W ) /\ ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) ) -> G e. T )
37 22 25 35 36 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> G e. T )
38 1 9 11 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. E /\ G e. T ) -> ( p ` G ) e. T )
39 22 23 37 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( p ` G ) e. T )
40 21 39 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> i e. T )
41 1 11 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. E /\ ( J ` s ) e. E ) -> ( p o. ( J ` s ) ) e. E )
42 22 23 30 41 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( p o. ( J ` s ) ) e. E )
43 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( K e. HL /\ W e. H ) )
44 24 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( P e. C /\ -. P .<_ W ) )
45 29 3adant2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( J ` s ) e. E )
46 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> f e. T )
47 43 45 46 32 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( ( J ` s ) ` f ) e. T )
48 43 47 44 34 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) )
49 43 44 48 36 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> G e. T )
50 6 7 1 9 20 ltrniotaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. C /\ -. P .<_ W ) /\ ( ( ( ( J ` s ) ` f ) ` P ) e. C /\ -. ( ( ( J ` s ) ` f ) ` P ) .<_ W ) ) -> ( G ` P ) = ( ( ( J ` s ) ` f ) ` P ) )
51 43 44 48 50 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( G ` P ) = ( ( ( J ` s ) ` f ) ` P ) )
52 6 7 1 9 cdlemd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ G e. T /\ ( ( J ` s ) ` f ) e. T ) /\ ( P e. C /\ -. P .<_ W ) /\ ( G ` P ) = ( ( ( J ` s ) ` f ) ` P ) ) -> G = ( ( J ` s ) ` f ) )
53 43 49 47 44 51 52 syl311anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> G = ( ( J ` s ) ` f ) )
54 53 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> G = ( ( J ` s ) ` f ) )
55 54 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( p ` G ) = ( p ` ( ( J ` s ) ` f ) ) )
56 1 9 11 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. E /\ ( J ` s ) e. E ) /\ f e. T ) -> ( ( p o. ( J ` s ) ) ` f ) = ( p ` ( ( J ` s ) ` f ) ) )
57 22 23 30 31 56 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( ( p o. ( J ` s ) ) ` f ) = ( p ` ( ( J ` s ) ` f ) ) )
58 55 21 57 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> i = ( ( p o. ( J ` s ) ) ` f ) )
59 coass 
 |-  ( ( p o. ( J ` s ) ) o. s ) = ( p o. ( ( J ` s ) o. s ) )
60 5 1 9 11 12 2 13 14 tendolinv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ s =/= O ) -> ( ( J ` s ) o. s ) = ( _I |` T ) )
61 22 26 27 60 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( ( J ` s ) o. s ) = ( _I |` T ) )
62 61 coeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( p o. ( ( J ` s ) o. s ) ) = ( p o. ( _I |` T ) ) )
63 1 9 11 tendo1mulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. E ) -> ( p o. ( _I |` T ) ) = p )
64 22 23 63 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( p o. ( _I |` T ) ) = p )
65 62 64 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( p o. ( ( J ` s ) o. s ) ) = p )
66 59 65 syl5req 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> p = ( ( p o. ( J ` s ) ) o. s ) )
67 fveq1 
 |-  ( t = ( p o. ( J ` s ) ) -> ( t ` f ) = ( ( p o. ( J ` s ) ) ` f ) )
68 67 eqeq2d 
 |-  ( t = ( p o. ( J ` s ) ) -> ( i = ( t ` f ) <-> i = ( ( p o. ( J ` s ) ) ` f ) ) )
69 coeq1 
 |-  ( t = ( p o. ( J ` s ) ) -> ( t o. s ) = ( ( p o. ( J ` s ) ) o. s ) )
70 69 eqeq2d 
 |-  ( t = ( p o. ( J ` s ) ) -> ( p = ( t o. s ) <-> p = ( ( p o. ( J ` s ) ) o. s ) ) )
71 68 70 anbi12d 
 |-  ( t = ( p o. ( J ` s ) ) -> ( ( i = ( t ` f ) /\ p = ( t o. s ) ) <-> ( i = ( ( p o. ( J ` s ) ) ` f ) /\ p = ( ( p o. ( J ` s ) ) o. s ) ) ) )
72 71 rspcev 
 |-  ( ( ( p o. ( J ` s ) ) e. E /\ ( i = ( ( p o. ( J ` s ) ) ` f ) /\ p = ( ( p o. ( J ` s ) ) o. s ) ) ) -> E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) )
73 42 58 66 72 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) )
74 40 23 73 jca31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i = ( p ` G ) /\ p e. E ) ) -> ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) )
75 simp3r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> p = ( t o. s ) )
76 75 fveq1d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( p ` ( ( J ` s ) ` f ) ) = ( ( t o. s ) ` ( ( J ` s ) ` f ) ) )
77 simp1l1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( K e. HL /\ W e. H ) )
78 simp2 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> t e. E )
79 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) -> s e. E )
80 79 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> s e. E )
81 1 11 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ t e. E /\ s e. E ) -> ( t o. s ) e. E )
82 77 78 80 81 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( t o. s ) e. E )
83 simp1l3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> s =/= O )
84 77 80 83 29 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( J ` s ) e. E )
85 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) -> f e. T )
86 85 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> f e. T )
87 1 9 11 tendocoval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( t o. s ) e. E /\ ( J ` s ) e. E ) /\ f e. T ) -> ( ( ( t o. s ) o. ( J ` s ) ) ` f ) = ( ( t o. s ) ` ( ( J ` s ) ` f ) ) )
88 77 82 84 86 87 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( ( ( t o. s ) o. ( J ` s ) ) ` f ) = ( ( t o. s ) ` ( ( J ` s ) ` f ) ) )
89 coass 
 |-  ( ( t o. s ) o. ( J ` s ) ) = ( t o. ( s o. ( J ` s ) ) )
90 5 1 9 11 12 2 13 14 tendorinv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ s =/= O ) -> ( s o. ( J ` s ) ) = ( _I |` T ) )
91 77 80 83 90 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( s o. ( J ` s ) ) = ( _I |` T ) )
92 91 coeq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( t o. ( s o. ( J ` s ) ) ) = ( t o. ( _I |` T ) ) )
93 1 9 11 tendo1mulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ t e. E ) -> ( t o. ( _I |` T ) ) = t )
94 77 78 93 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( t o. ( _I |` T ) ) = t )
95 92 94 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( t o. ( s o. ( J ` s ) ) ) = t )
96 89 95 syl5eq 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( ( t o. s ) o. ( J ` s ) ) = t )
97 96 fveq1d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( ( ( t o. s ) o. ( J ` s ) ) ` f ) = ( t ` f ) )
98 76 88 97 3eqtr2rd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( t ` f ) = ( p ` ( ( J ` s ) ` f ) ) )
99 simp3l 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> i = ( t ` f ) )
100 53 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) -> G = ( ( J ` s ) ` f ) )
101 100 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> G = ( ( J ` s ) ` f ) )
102 101 fveq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> ( p ` G ) = ( p ` ( ( J ` s ) ` f ) ) )
103 98 99 102 3eqtr4d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) /\ t e. E /\ ( i = ( t ` f ) /\ p = ( t o. s ) ) ) -> i = ( p ` G ) )
104 103 rexlimdv3a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) -> ( E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) -> i = ( p ` G ) ) )
105 104 impr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) ) -> i = ( p ` G ) )
106 simprlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) ) -> p e. E )
107 105 106 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) ) -> ( i = ( p ` G ) /\ p e. E ) )
108 74 107 impbida 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( ( i = ( p ` G ) /\ p e. E ) <-> ( ( i e. T /\ p e. E ) /\ E. t e. E ( i = ( t ` f ) /\ p = ( t o. s ) ) ) ) )