# Metamath Proof Explorer

## Theorem hvmapffval

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

Ref Expression
Hypothesis hvmapval.h
`|- H = ( LHyp ` K )`
Assertion hvmapffval
`|- ( K e. X -> ( HVMap ` K ) = ( w e. H |-> ( x e. ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) ) ) ) )`

### Proof

Step Hyp Ref Expression
1 hvmapval.h
` |-  H = ( LHyp ` K )`
2 elex
` |-  ( K e. X -> K e. _V )`
3 fveq2
` |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )`
4 3 1 syl6eqr
` |-  ( k = K -> ( LHyp ` k ) = H )`
5 fveq2
` |-  ( k = K -> ( DVecH ` k ) = ( DVecH ` K ) )`
6 5 fveq1d
` |-  ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )`
7 6 fveq2d
` |-  ( k = K -> ( Base ` ( ( DVecH ` k ) ` w ) ) = ( Base ` ( ( DVecH ` K ) ` w ) ) )`
8 6 fveq2d
` |-  ( k = K -> ( 0g ` ( ( DVecH ` k ) ` w ) ) = ( 0g ` ( ( DVecH ` K ) ` w ) ) )`
9 8 sneqd
` |-  ( k = K -> { ( 0g ` ( ( DVecH ` k ) ` w ) ) } = { ( 0g ` ( ( DVecH ` K ) ` w ) ) } )`
10 7 9 difeq12d
` |-  ( k = K -> ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) = ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) )`
11 6 fveq2d
` |-  ( k = K -> ( Scalar ` ( ( DVecH ` k ) ` w ) ) = ( Scalar ` ( ( DVecH ` K ) ` w ) ) )`
12 11 fveq2d
` |-  ( k = K -> ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) = ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) )`
13 fveq2
` |-  ( k = K -> ( ocH ` k ) = ( ocH ` K ) )`
14 13 fveq1d
` |-  ( k = K -> ( ( ocH ` k ) ` w ) = ( ( ocH ` K ) ` w ) )`
15 14 fveq1d
` |-  ( k = K -> ( ( ( ocH ` k ) ` w ) ` { x } ) = ( ( ( ocH ` K ) ` w ) ` { x } ) )`
16 6 fveq2d
` |-  ( k = K -> ( +g ` ( ( DVecH ` k ) ` w ) ) = ( +g ` ( ( DVecH ` K ) ` w ) ) )`
17 eqidd
` |-  ( k = K -> t = t )`
18 6 fveq2d
` |-  ( k = K -> ( .s ` ( ( DVecH ` k ) ` w ) ) = ( .s ` ( ( DVecH ` K ) ` w ) ) )`
19 18 oveqd
` |-  ( k = K -> ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) = ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) )`
20 16 17 19 oveq123d
` |-  ( k = K -> ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) )`
21 20 eqeq2d
` |-  ( k = K -> ( v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) <-> v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) )`
22 15 21 rexeqbidv
` |-  ( k = K -> ( E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) <-> E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) )`
23 12 22 riotaeqbidv
` |-  ( k = K -> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) = ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) )`
24 7 23 mpteq12dv
` |-  ( k = K -> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) = ( v e. ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) ) )`
25 10 24 mpteq12dv
` |-  ( k = K -> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) = ( x e. ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) ) ) )`
26 4 25 mpteq12dv
` |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) ) = ( w e. H |-> ( x e. ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) ) ) ) )`
27 df-hvmap
` |-  HVMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( ( Base ` ( ( DVecH ` k ) ` w ) ) \ { ( 0g ` ( ( DVecH ` k ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` k ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` k ) ` w ) ) ) E. t e. ( ( ( ocH ` k ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` k ) ` w ) ) ( j ( .s ` ( ( DVecH ` k ) ` w ) ) x ) ) ) ) ) ) )`
28 26 27 1 mptfvmpt
` |-  ( K e. _V -> ( HVMap ` K ) = ( w e. H |-> ( x e. ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) ) ) ) )`
29 2 28 syl
` |-  ( K e. X -> ( HVMap ` K ) = ( w e. H |-> ( x e. ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) |-> ( v e. ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( iota_ j e. ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) ) ) ) ) )`