Metamath Proof Explorer

Theorem hvmapvalvalN

Description: Value of value of map (i.e. functional value) from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015) (New usage is discouraged.)

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. } ) )
hvmapval.y 
|- ( ph -> Y e. V )
Assertion hvmapvalvalN 
|- ( ph -> ( ( M ` X ) ` Y ) = ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( 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 hvmapval.y 
 |-  ( ph -> Y e. V )
14 1 2 3 4 5 6 7 8 9 10 11 12 hvmapval 
 |-  ( ph -> ( M ` X ) = ( y e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) ) ) )
15 14 fveq1d 
 |-  ( ph -> ( ( M ` X ) ` Y ) = ( ( y e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) ) ) ` Y ) )
16 riotaex 
 |-  ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) e. _V
17 eqeq1 
 |-  ( y = Y -> ( y = ( t .+ ( j .x. X ) ) <-> Y = ( t .+ ( j .x. X ) ) ) )
18 17 rexbidv 
 |-  ( y = Y -> ( E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) <-> E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) )
19 18 riotabidv 
 |-  ( y = Y -> ( iota_ j e. R E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) ) = ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) )
20 eqid 
 |-  ( y e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) ) ) = ( y e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) ) )
21 19 20 fvmptg 
 |-  ( ( Y e. V /\ ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) e. _V ) -> ( ( y e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) ) ) ` Y ) = ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) )
22 13 16 21 sylancl 
 |-  ( ph -> ( ( y e. V |-> ( iota_ j e. R E. t e. ( O ` { X } ) y = ( t .+ ( j .x. X ) ) ) ) ` Y ) = ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) )
23 15 22 eqtrd 
 |-  ( ph -> ( ( M ` X ) ` Y ) = ( iota_ j e. R E. t e. ( O ` { X } ) Y = ( t .+ ( j .x. X ) ) ) )