Metamath Proof Explorer

Theorem hvmapfval

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

Ref Expression
Hypotheses hvmapval.h 
|- H = ( LHyp ` K )
hvmapval.u 
|- U = ( ( DVecH ` K ) ` W )
hvmapval.o 
|- O = ( ( ocH ` K ) ` W )
hvmapval.v 
|- V = ( Base ` U )
hvmapval.p 
|- .+ = ( +g ` U )
hvmapval.t 
|- .x. = ( .s ` U )
hvmapval.z 
|- .0. = ( 0g ` U )
hvmapval.s 
|- S = ( Scalar ` U )
hvmapval.r 
|- R = ( Base ` S )
hvmapval.m 
|- M = ( ( HVMap ` K ) ` W )
hvmapval.k 
|- ( ph -> ( K e. A /\ W e. H ) )
Assertion hvmapfval 
|- ( ph -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hvmapval.h 
 |-  H = ( LHyp ` K )
2 hvmapval.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hvmapval.o 
 |-  O = ( ( ocH ` K ) ` W )
4 hvmapval.v 
 |-  V = ( Base ` U )
5 hvmapval.p 
 |-  .+ = ( +g ` U )
6 hvmapval.t 
 |-  .x. = ( .s ` U )
7 hvmapval.z 
 |-  .0. = ( 0g ` U )
8 hvmapval.s 
 |-  S = ( Scalar ` U )
9 hvmapval.r 
 |-  R = ( Base ` S )
10 hvmapval.m 
 |-  M = ( ( HVMap ` K ) ` W )
11 hvmapval.k 
 |-  ( ph -> ( K e. A /\ W e. H ) )
12 1 hvmapffval 
 |-  ( K e. A -> ( 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 ) ) ) ) ) ) )
13 12 fveq1d 
 |-  ( K e. A -> ( ( HVMap ` K ) ` W ) = ( ( 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 ) ) ) ) ) ) ` W ) )
14 10 13 syl5eq 
 |-  ( K e. A -> M = ( ( 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 ) ) ) ) ) ) ` W ) )
15 fveq2 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
16 15 2 eqtr4di 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = U )
17 16 fveq2d 
 |-  ( w = W -> ( Base ` ( ( DVecH ` K ) ` w ) ) = ( Base ` U ) )
18 17 4 eqtr4di 
 |-  ( w = W -> ( Base ` ( ( DVecH ` K ) ` w ) ) = V )
19 16 fveq2d 
 |-  ( w = W -> ( 0g ` ( ( DVecH ` K ) ` w ) ) = ( 0g ` U ) )
20 19 7 eqtr4di 
 |-  ( w = W -> ( 0g ` ( ( DVecH ` K ) ` w ) ) = .0. )
21 20 sneqd 
 |-  ( w = W -> { ( 0g ` ( ( DVecH ` K ) ` w ) ) } = { .0. } )
22 18 21 difeq12d 
 |-  ( w = W -> ( ( Base ` ( ( DVecH ` K ) ` w ) ) \ { ( 0g ` ( ( DVecH ` K ) ` w ) ) } ) = ( V \ { .0. } ) )
23 16 fveq2d 
 |-  ( w = W -> ( Scalar ` ( ( DVecH ` K ) ` w ) ) = ( Scalar ` U ) )
24 23 8 eqtr4di 
 |-  ( w = W -> ( Scalar ` ( ( DVecH ` K ) ` w ) ) = S )
25 24 fveq2d 
 |-  ( w = W -> ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) = ( Base ` S ) )
26 25 9 eqtr4di 
 |-  ( w = W -> ( Base ` ( Scalar ` ( ( DVecH ` K ) ` w ) ) ) = R )
27 fveq2 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = ( ( ocH ` K ) ` W ) )
28 27 3 eqtr4di 
 |-  ( w = W -> ( ( ocH ` K ) ` w ) = O )
29 28 fveq1d 
 |-  ( w = W -> ( ( ( ocH ` K ) ` w ) ` { x } ) = ( O ` { x } ) )
30 16 fveq2d 
 |-  ( w = W -> ( +g ` ( ( DVecH ` K ) ` w ) ) = ( +g ` U ) )
31 30 5 eqtr4di 
 |-  ( w = W -> ( +g ` ( ( DVecH ` K ) ` w ) ) = .+ )
32 eqidd 
 |-  ( w = W -> t = t )
33 16 fveq2d 
 |-  ( w = W -> ( .s ` ( ( DVecH ` K ) ` w ) ) = ( .s ` U ) )
34 33 6 eqtr4di 
 |-  ( w = W -> ( .s ` ( ( DVecH ` K ) ` w ) ) = .x. )
35 34 oveqd 
 |-  ( w = W -> ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) = ( j .x. x ) )
36 31 32 35 oveq123d 
 |-  ( w = W -> ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) = ( t .+ ( j .x. x ) ) )
37 36 eqeq2d 
 |-  ( w = W -> ( v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) <-> v = ( t .+ ( j .x. x ) ) ) )
38 29 37 rexeqbidv 
 |-  ( w = W -> ( E. t e. ( ( ( ocH ` K ) ` w ) ` { x } ) v = ( t ( +g ` ( ( DVecH ` K ) ` w ) ) ( j ( .s ` ( ( DVecH ` K ) ` w ) ) x ) ) <-> E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) )
39 26 38 riotaeqbidv 
 |-  ( w = 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 ) ) ) = ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) )
40 18 39 mpteq12dv 
 |-  ( w = 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 ) ) ) ) = ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) )
41 22 40 mpteq12dv 
 |-  ( w = W -> ( 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. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) )
42 eqid 
 |-  ( 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 ) ) ) ) ) ) = ( 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 ) ) ) ) ) )
43 4 fvexi 
 |-  V e. _V
44 43 difexi 
 |-  ( V \ { .0. } ) e. _V
45 44 mptex 
 |-  ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) e. _V
46 41 42 45 fvmpt 
 |-  ( W e. H -> ( ( 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 ) ) ) ) ) ) ` W ) = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) )
47 14 46 sylan9eq 
 |-  ( ( K e. A /\ W e. H ) -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) )
48 11 47 syl 
 |-  ( ph -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) )