# 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 )`