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 eqtr2id
 |-  ( ( ( ( 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 ) ) ) ) )