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 eqtr4di 
 |-  ( 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 ) ) ) ) ) ) )