Metamath Proof Explorer

Theorem hdmapfnN

Description: Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmapfn.h 
|- H = ( LHyp ` K )
hdmapfn.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapfn.v 
|- V = ( Base ` U )
hdmapfn.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapfn.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hdmapfnN 
|- ( ph -> S Fn V )

Proof

Step Hyp Ref Expression
1 hdmapfn.h 
 |-  H = ( LHyp ` K )
2 hdmapfn.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmapfn.v 
 |-  V = ( Base ` U )
4 hdmapfn.s 
 |-  S = ( ( HDMap ` K ) ` W )
5 hdmapfn.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 riotaex 
 |-  ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. V ( -. z e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { t } ) ) -> y = ( ( ( HDMap1 ` K ) ` W ) ` <. z , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , z >. ) , t >. ) ) ) e. _V
7 eqid 
 |-  ( t e. V |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. V ( -. z e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { t } ) ) -> y = ( ( ( HDMap1 ` K ) ` W ) ` <. z , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , z >. ) , t >. ) ) ) ) = ( t e. V |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. V ( -. z e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { t } ) ) -> y = ( ( ( HDMap1 ` K ) ` W ) ` <. z , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , z >. ) , t >. ) ) ) )
8 6 7 fnmpti 
 |-  ( t e. V |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. V ( -. z e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { t } ) ) -> y = ( ( ( HDMap1 ` K ) ` W ) ` <. z , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , z >. ) , t >. ) ) ) ) Fn V
9 eqid 
 |-  <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
10 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
11 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
12 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
13 eqid 
 |-  ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
14 eqid 
 |-  ( ( HDMap1 ` K ) ` W ) = ( ( HDMap1 ` K ) ` W )
15 1 9 2 3 10 11 12 13 14 4 5 hdmapfval 
 |-  ( ph -> S = ( t e. V |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. V ( -. z e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { t } ) ) -> y = ( ( ( HDMap1 ` K ) ` W ) ` <. z , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , z >. ) , t >. ) ) ) ) )
16 15 fneq1d 
 |-  ( ph -> ( S Fn V <-> ( t e. V |-> ( iota_ y e. ( Base ` ( ( LCDual ` K ) ` W ) ) A. z e. V ( -. z e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { t } ) ) -> y = ( ( ( HDMap1 ` K ) ` W ) ` <. z , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , z >. ) , t >. ) ) ) ) Fn V ) )
17 8 16 mpbiri 
 |-  ( ph -> S Fn V )