Metamath Proof Explorer

Theorem ldualfvs

Description: Scalar product operation 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 )
ldualfvs.m 
|- .x. = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) )
Assertion ldualfvs 
|- ( ph -> .xb = .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 ldualfvs.m 
 |-  .x. = ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) )
10 eqid 
 |-  ( +g ` R ) = ( +g ` R )
11 eqid 
 |-  ( oF ( +g ` R ) |` ( F X. F ) ) = ( oF ( +g ` R ) |` ( F X. F ) )
12 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
13 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 } ) ) )
14 2 10 11 1 6 3 4 5 12 13 8 ldualset 
 |-  ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) >. } ) )
15 14 fveq2d 
 |-  ( ph -> ( .s ` D ) = ( .s ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) >. } ) ) )
16 4 fvexi 
 |-  K e. _V
17 1 fvexi 
 |-  F e. _V
18 16 17 mpoex 
 |-  ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) e. _V
19 eqid 
 |-  ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) >. } ) = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) >. } )
20 19 lmodvsca 
 |-  ( ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) e. _V -> ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) = ( .s ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) >. } ) ) )
21 18 20 ax-mp 
 |-  ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) = ( .s ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) >. } ) )
22 9 21 eqtri 
 |-  .x. = ( .s ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` R ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. K , f e. F |-> ( f oF .X. ( V X. { k } ) ) ) >. } ) )
23 15 7 22 3eqtr4g 
 |-  ( ph -> .xb = .x. )