Metamath Proof Explorer

Theorem hdmapffval

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

Ref Expression
Hypothesis hdmapval.h 
|- H = ( LHyp ` K )
Assertion hdmapffval 
|- ( K e. X -> ( 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 >. ) ) ) ) } ) )

Proof

Step Hyp Ref Expression
1 hdmapval.h 
 |-  H = ( LHyp ` K )
2 elex 
 |-  ( K e. X -> K e. _V )
3 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
4 3 1 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
5 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
6 5 reseq2d 
 |-  ( k = K -> ( _I |` ( Base ` k ) ) = ( _I |` ( Base ` K ) ) )
7 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
8 7 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
9 8 reseq2d 
 |-  ( k = K -> ( _I |` ( ( LTrn ` k ) ` w ) ) = ( _I |` ( ( LTrn ` K ) ` w ) ) )
10 6 9 opeq12d 
 |-  ( k = K -> <. ( _I |` ( Base ` k ) ) , ( _I |` ( ( LTrn ` k ) ` w ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. )
11 fveq2 
 |-  ( k = K -> ( DVecH ` k ) = ( DVecH ` K ) )
12 11 fveq1d 
 |-  ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )
13 fveq2 
 |-  ( k = K -> ( HDMap1 ` k ) = ( HDMap1 ` K ) )
14 13 fveq1d 
 |-  ( k = K -> ( ( HDMap1 ` k ) ` w ) = ( ( HDMap1 ` K ) ` w ) )
15 fveq2 
 |-  ( k = K -> ( LCDual ` k ) = ( LCDual ` K ) )
16 15 fveq1d 
 |-  ( k = K -> ( ( LCDual ` k ) ` w ) = ( ( LCDual ` K ) ` w ) )
17 16 fveq2d 
 |-  ( k = K -> ( Base ` ( ( LCDual ` k ) ` w ) ) = ( Base ` ( ( LCDual ` K ) ` w ) ) )
18 fveq2 
 |-  ( k = K -> ( HVMap ` k ) = ( HVMap ` K ) )
19 18 fveq1d 
 |-  ( k = K -> ( ( HVMap ` k ) ` w ) = ( ( HVMap ` K ) ` w ) )
20 19 fveq1d 
 |-  ( k = K -> ( ( ( HVMap ` k ) ` w ) ` e ) = ( ( ( HVMap ` K ) ` w ) ` e ) )
21 20 oteq2d 
 |-  ( k = K -> <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. = <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. )
22 21 fveq2d 
 |-  ( k = K -> ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) = ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) )
23 22 oteq2d 
 |-  ( k = K -> <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. = <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. )
24 23 fveq2d 
 |-  ( k = K -> ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) )
25 24 eqeq2d 
 |-  ( k = K -> ( y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` k ) ` w ) ` e ) , z >. ) , t >. ) <-> y = ( i ` <. z , ( i ` <. e , ( ( ( HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) )
26 25 imbi2d 
 |-  ( k = K -> ( ( -. 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 >. ) ) ) )
27 26 ralbidv 
 |-  ( k = K -> ( 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 >. ) ) ) )
28 17 27 riotaeqbidv 
 |-  ( k = K -> ( 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 >. ) ) ) )
29 28 mpteq2dv 
 |-  ( k = K -> ( 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 >. ) ) ) ) )
30 29 eleq2d 
 |-  ( k = K -> ( 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 >. ) ) ) ) ) )
31 14 30 sbceqbid 
 |-  ( k = K -> ( [. ( ( 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 >. ) ) ) ) ) )
32 31 sbcbidv 
 |-  ( k = K -> ( [. ( 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 >. ) ) ) ) ) )
33 12 32 sbceqbid 
 |-  ( k = K -> ( [. ( ( 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 >. ) ) ) ) ) )
34 10 33 sbceqbid 
 |-  ( k = K -> ( [. <. ( _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 >. ) ) ) ) ) )
35 34 abbidv 
 |-  ( k = K -> { 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 >. ) ) ) ) } = { 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 >. ) ) ) ) } )
36 4 35 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> { 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 >. ) ) ) ) } ) )
37 df-hdmap 
 |-  HDMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { 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 >. ) ) ) ) } ) )
38 36 37 1 mptfvmpt 
 |-  ( K e. _V -> ( 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 >. ) ) ) ) } ) )
39 2 38 syl 
 |-  ( K e. X -> ( 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 >. ) ) ) ) } ) )