Metamath Proof Explorer

Theorem ldualvs

Description: Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualfvs.f 
|- F = ( LFnl ` W )
ldualfvs.v 
|- V = ( Base ` W )
ldualfvs.r 
|- R = ( Scalar ` W )
ldualfvs.k 
|- K = ( Base ` R )
ldualfvs.t 
|- .X. = ( .r ` R )
ldualfvs.d 
|- D = ( LDual ` W )
ldualfvs.s 
|- .xb = ( .s ` D )
ldualfvs.w 
|- ( ph -> W e. Y )
ldualvs.x 
|- ( ph -> X e. K )
ldualvs.g 
|- ( ph -> G e. F )
Assertion ldualvs 
|- ( ph -> ( X .xb G ) = ( G oF .X. ( V X. { X } ) ) )

Proof

Step Hyp Ref Expression
1 ldualfvs.f 
 |-  F = ( LFnl ` W )
2 ldualfvs.v 
 |-  V = ( Base ` W )
3 ldualfvs.r 
 |-  R = ( Scalar ` W )
4 ldualfvs.k 
 |-  K = ( Base ` R )
5 ldualfvs.t 
 |-  .X. = ( .r ` R )
6 ldualfvs.d 
 |-  D = ( LDual ` W )
7 ldualfvs.s 
 |-  .xb = ( .s ` D )
8 ldualfvs.w 
 |-  ( ph -> W e. Y )
9 ldualvs.x 
 |-  ( ph -> X e. K )
10 ldualvs.g 
 |-  ( ph -> G e. F )
11 eqid 
 |-  ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) )
12 1 2 3 4 5 6 7 8 11 ldualfvs 
 |-  ( ph -> .xb = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) )
13 12 oveqd 
 |-  ( ph -> ( X .xb G ) = ( X ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) G ) )
14 sneq 
 |-  ( k = X -> { k } = { X } )
15 14 xpeq2d 
 |-  ( k = X -> ( V X. { k } ) = ( V X. { X } ) )
16 15 oveq2d 
 |-  ( k = X -> ( f oF .X. ( V X. { k } ) ) = ( f oF .X. ( V X. { X } ) ) )
17 oveq1 
 |-  ( f = G -> ( f oF .X. ( V X. { X } ) ) = ( G oF .X. ( V X. { X } ) ) )
18 ovex 
 |-  ( G oF .X. ( V X. { X } ) ) e. _V
19 16 17 11 18 ovmpo 
 |-  ( ( X e. K /\ G e. F ) -> ( X ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) G ) = ( G oF .X. ( V X. { X } ) ) )
20 9 10 19 syl2anc 
 |-  ( ph -> ( X ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) G ) = ( G oF .X. ( V X. { X } ) ) )
21 13 20 eqtrd 
 |-  ( ph -> ( X .xb G ) = ( G oF .X. ( V X. { X } ) ) )