Metamath Proof Explorer

Theorem hvmapval

Description: Value of 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 ) )
hvmapval.x 
|- ( ph -> X e. ( V \ { .0. } ) )
Assertion hvmapval 
|- ( ph -> ( M ` X ) = ( 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 hvmapval.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
13 1 2 3 4 5 6 7 8 9 10 11 hvmapfval 
 |-  ( ph -> M = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) )
14 13 fveq1d 
 |-  ( ph -> ( M ` X ) = ( ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) ` X ) )
15 4 fvexi 
 |-  V e. _V
16 15 mptex 
 |-  ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) ) e. _V
17 sneq 
 |-  ( x = X -> { x } = { X } )
18 17 fveq2d 
 |-  ( x = X -> ( O ` { x } ) = ( O ` { X } ) )
19 oveq2 
 |-  ( x = X -> ( j .x. x ) = ( j .x. X ) )
20 19 oveq2d 
 |-  ( x = X -> ( t .+ ( j .x. x ) ) = ( t .+ ( j .x. X ) ) )
21 20 eqeq2d 
 |-  ( x = X -> ( v = ( t .+ ( j .x. x ) ) <-> v = ( t .+ ( j .x. X ) ) ) )
22 18 21 rexeqbidv 
 |-  ( x = X -> ( E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) <-> E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) )
23 22 riotabidv 
 |-  ( x = X -> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) = ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) )
24 23 mpteq2dv 
 |-  ( x = X -> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) = ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) ) )
25 eqid 
 |-  ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) = ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) )
26 24 25 fvmptg 
 |-  ( ( X e. ( V \ { .0. } ) /\ ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) ) e. _V ) -> ( ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) ` X ) = ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) ) )
27 12 16 26 sylancl 
 |-  ( ph -> ( ( x e. ( V \ { .0. } ) |-> ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { x } ) v = ( t .+ ( j .x. x ) ) ) ) ) ` X ) = ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) ) )
28 14 27 eqtrd 
 |-  ( ph -> ( M ` X ) = ( v e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) v = ( t .+ ( j .x. X ) ) ) ) )