# 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 ) )`
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) -> ( P e. C /\ -. P .<_ W ) )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( f e. T /\ s e. E ) /\ s =/= O ) /\ ( i e. T /\ p e. E ) ) -> G = ( ( J ` s ) ` f ) )`
` |-  ( ( ( ( ( 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 ) ) ) ) )`