Metamath Proof Explorer

Theorem hdmapfval

Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapval.h 
|- H = ( LHyp ` K )
hdmapfval.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapfval.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapfval.v 
|- V = ( Base ` U )
hdmapfval.n 
|- N = ( LSpan ` U )
hdmapfval.c 
|- C = ( ( LCDual ` K ) ` W )
hdmapfval.d 
|- D = ( Base ` C )
hdmapfval.j 
|- J = ( ( HVMap ` K ) ` W )
hdmapfval.i 
|- I = ( ( HDMap1 ` K ) ` W )
hdmapfval.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapfval.k 
|- ( ph -> ( K e. A /\ W e. H ) )
Assertion hdmapfval 
|- ( ph -> S = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hdmapval.h 
 |-  H = ( LHyp ` K )
2 hdmapfval.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapfval.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 hdmapfval.v 
 |-  V = ( Base ` U )
5 hdmapfval.n 
 |-  N = ( LSpan ` U )
6 hdmapfval.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 hdmapfval.d 
 |-  D = ( Base ` C )
8 hdmapfval.j 
 |-  J = ( ( HVMap ` K ) ` W )
9 hdmapfval.i 
 |-  I = ( ( HDMap1 ` K ) ` W )
10 hdmapfval.s 
 |-  S = ( ( HDMap ` K ) ` W )
11 hdmapfval.k 
 |-  ( ph -> ( K e. A /\ W e. H ) )
12 1 hdmapffval 
 |-  ( K e. A -> ( HDMap ` K ) = ( w e. H |-> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) )
13 12 fveq1d 
 |-  ( K e. A -> ( ( HDMap ` K ) ` W ) = ( ( w e. H |-> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) ` W ) )
14 10 13 eqtrid 
 |-  ( K e. A -> S = ( ( w e. H |-> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) ` W ) )
15 fveq2 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) )
16 15 reseq2d 
 |-  ( w = W -> ( _I |` ( ( LTrn ` K ) ` w ) ) = ( _I |` ( ( LTrn ` K ) ` W ) ) )
17 16 opeq2d 
 |-  ( w = W -> <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. )
18 fveq2 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
19 fveq2 
 |-  ( w = W -> ( ( HDMap1 ` K ) ` w ) = ( ( HDMap1 ` K ) ` W ) )
20 2fveq3 
 |-  ( w = W -> ( Base ` ( ( LCDual ` K ) ` w ) ) = ( Base ` ( ( LCDual ` K ) ` W ) ) )
21 fveq2 
 |-  ( w = W -> ( ( HVMap ` K ) ` w ) = ( ( HVMap ` K ) ` W ) )
22 21 fveq1d 
 |-  ( w = W -> ( ( ( HVMap ` K ) ` w ) ` e ) = ( ( ( HVMap ` K ) ` W ) ` e ) )
23 22 oteq2d 
 |-  ( w = W -> <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. = <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. )
24 23 fveq2d 
 |-  ( w = W -> ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) = ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) )
25 24 oteq2d 
 |-  ( w = W -> <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. = <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. )
26 25 fveq2d 
 |-  ( w = W -> ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) )
27 26 eqeq2d 
 |-  ( w = W -> ( y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) <-> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) )
28 27 imbi2d 
 |-  ( w = W -> ( ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) <-> ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) )
29 28 ralbidv 
 |-  ( w = W -> ( A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) <-> A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) )
30 20 29 riotaeqbidv 
 |-  ( w = W -> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) = ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) )
31 30 mpteq2dv 
 |-  ( w = W -> ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) = ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) )
32 31 eleq2d 
 |-  ( w = W -> ( a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) ) )
33 19 32 sbceqbid 
 |-  ( w = W -> ( [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) <-> [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) ) )
34 33 sbcbidv 
 |-  ( w = W -> ( [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) <-> [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) ) )
35 18 34 sbceqbid 
 |-  ( w = W -> ( [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) <-> [. ( ( DVecH ` K ) ` W ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) ) )
36 17 35 sbceqbid 
 |-  ( w = W -> ( [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) <-> [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. / e ]. [. ( ( DVecH ` K ) ` W ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) ) )
37 opex 
 |-  <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. _V
38 fvex 
 |-  ( ( DVecH ` K ) ` W ) e. _V
39 fvex 
 |-  ( Base ` u ) e. _V
40 simp1 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. )
41 40 2 eqtr4di 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> e = E )
42 simp2 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> u = ( ( DVecH ` K ) ` W ) )
43 42 3 eqtr4di 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> u = U )
44 simp3 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> v = ( Base ` u ) )
45 43 fveq2d 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> ( Base ` u ) = ( Base ` U ) )
46 44 45 eqtrd 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> v = ( Base ` U ) )
47 46 4 eqtr4di 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> v = V )
48 fvex 
 |-  ( ( HDMap1 ` K ) ` W ) e. _V
49 id 
 |-  ( i = ( ( HDMap1 ` K ) ` W ) -> i = ( ( HDMap1 ` K ) ` W ) )
50 49 9 eqtr4di 
 |-  ( i = ( ( HDMap1 ` K ) ` W ) -> i = I )
51 fveq1 
 |-  ( i = I -> ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) = ( I ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) )
52 fveq1 
 |-  ( i = I -> ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) = ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) )
53 52 oteq2d 
 |-  ( i = I -> <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. = <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. )
54 53 fveq2d 
 |-  ( i = I -> ( I ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) )
55 51 54 eqtrd 
 |-  ( i = I -> ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) )
56 55 eqeq2d 
 |-  ( i = I -> ( y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) <-> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) )
57 56 imbi2d 
 |-  ( i = I -> ( ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) <-> ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) )
58 57 ralbidv 
 |-  ( i = I -> ( A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) <-> A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) )
59 58 riotabidv 
 |-  ( i = I -> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) = ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) )
60 59 mpteq2dv 
 |-  ( i = I -> ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) = ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) )
61 60 eleq2d 
 |-  ( i = I -> ( a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) ) )
62 50 61 syl 
 |-  ( i = ( ( HDMap1 ` K ) ` W ) -> ( a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) ) )
63 48 62 sbcie 
 |-  ( [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) )
64 simp3 
 |-  ( ( e = E /\ u = U /\ v = V ) -> v = V )
65 6 fveq2i 
 |-  ( Base ` C ) = ( Base ` ( ( LCDual ` K ) ` W ) )
66 7 65 eqtr2i 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = D
67 66 a1i 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( Base ` ( ( LCDual ` K ) ` W ) ) = D )
68 simp2 
 |-  ( ( e = E /\ u = U /\ v = V ) -> u = U )
69 68 fveq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( LSpan ` u ) = ( LSpan ` U ) )
70 69 5 eqtr4di 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( LSpan ` u ) = N )
71 simp1 
 |-  ( ( e = E /\ u = U /\ v = V ) -> e = E )
72 71 sneqd 
 |-  ( ( e = E /\ u = U /\ v = V ) -> { e } = { E } )
73 70 72 fveq12d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( ( LSpan ` u ) ` { e } ) = ( N ` { E } ) )
74 70 fveq1d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( ( LSpan ` u ) ` { t } ) = ( N ` { t } ) )
75 73 74 uneq12d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) = ( ( N ` { E } ) u. ( N ` { t } ) ) )
76 75 eleq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) <-> z e. ( ( N ` { E } ) u. ( N ` { t } ) ) ) )
77 76 notbid 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) <-> -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) ) )
78 71 oteq1d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. = <. E , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. )
79 71 fveq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( ( ( HVMap ` K ) ` W ) ` e ) = ( ( ( HVMap ` K ) ` W ) ` E ) )
80 8 fveq1i 
 |-  ( J ` E ) = ( ( ( HVMap ` K ) ` W ) ` E )
81 79 80 eqtr4di 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( ( ( HVMap ` K ) ` W ) ` e ) = ( J ` E ) )
82 81 oteq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> <. E , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. = <. E , ( J ` E ) , z >. )
83 78 82 eqtrd 
 |-  ( ( e = E /\ u = U /\ v = V ) -> <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. = <. E , ( J ` E ) , z >. )
84 83 fveq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) = ( I ` <. E , ( J ` E ) , z >. ) )
85 84 oteq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. = <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. )
86 85 fveq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) )
87 86 eqeq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) <-> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) )
88 77 87 imbi12d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) <-> ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) )
89 64 88 raleqbidv 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) )
90 67 89 riotaeqbidv 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) = ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) )
91 64 90 mpteq12dv 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )
92 91 eleq2d 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( I ` <. z , ( I ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ) )
93 63 92 bitrid 
 |-  ( ( e = E /\ u = U /\ v = V ) -> ( [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ) )
94 41 43 47 93 syl3anc 
 |-  ( ( e = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. /\ u = ( ( DVecH ` K ) ` W ) /\ v = ( Base ` u ) ) -> ( [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ) )
95 37 38 39 94 sbc3ie 
 |-  ( [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. / e ]. [. ( ( DVecH ` K ) ` W ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` W ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` W ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )
96 36 95 bitrdi 
 |-  ( w = W -> ( [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) <-> a e. ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ) )
97 96 eqabcdv 
 |-  ( w = W -> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )
98 eqid 
 |-  ( w e. H |-> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) = ( w e. H |-> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } )
99 97 98 4 mptfvmpt 
 |-  ( W e. H -> ( ( w e. H |-> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( ( HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) ` W ) = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )
100 14 99 sylan9eq 
 |-  ( ( K e. A /\ W e. H ) -> S = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )
101 11 100 syl 
 |-  ( ph -> S = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )