Metamath Proof Explorer

Theorem ldualvsval

Description: Value of scalar product operation value 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 )
ldualvs.a 
|- ( ph -> A e. V )
Assertion ldualvsval 
|- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .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 ldualvs.a 
 |-  ( ph -> A e. V )
12 1 2 3 4 5 6 7 8 9 10 ldualvs 
 |-  ( ph -> ( X .xb G ) = ( G oF .X. ( V X. { X } ) ) )
13 12 fveq1d 
 |-  ( ph -> ( ( X .xb G ) ` A ) = ( ( G oF .X. ( V X. { X } ) ) ` A ) )
14 2 fvexi 
 |-  V e. _V
15 14 a1i 
 |-  ( ph -> V e. _V )
16 3 4 2 1 lflf 
 |-  ( ( W e. Y /\ G e. F ) -> G : V --> K )
17 8 10 16 syl2anc 
 |-  ( ph -> G : V --> K )
18 17 ffnd 
 |-  ( ph -> G Fn V )
19 eqidd 
 |-  ( ( ph /\ A e. V ) -> ( G ` A ) = ( G ` A ) )
20 15 9 18 19 ofc2 
 |-  ( ( ph /\ A e. V ) -> ( ( G oF .X. ( V X. { X } ) ) ` A ) = ( ( G ` A ) .X. X ) )
21 11 20 mpdan 
 |-  ( ph -> ( ( G oF .X. ( V X. { X } ) ) ` A ) = ( ( G ` A ) .X. X ) )
22 13 21 eqtrd 
 |-  ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .X. X ) )