Metamath Proof Explorer

Theorem ldualvbase

Description: The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualvbase.f 
|- F = ( LFnl ` W )
ldualvbase.d 
|- D = ( LDual ` W )
ldualvbase.v 
|- V = ( Base ` D )
ldualvbase.w 
|- ( ph -> W e. X )
Assertion ldualvbase 
|- ( ph -> V = F )

Proof

Step Hyp Ref Expression
1 ldualvbase.f 
 |-  F = ( LFnl ` W )
2 ldualvbase.d 
 |-  D = ( LDual ` W )
3 ldualvbase.v 
 |-  V = ( Base ` D )
4 ldualvbase.w 
 |-  ( ph -> W e. X )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
7 eqid 
 |-  ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) ) = ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) )
8 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
9 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
10 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
11 eqid 
 |-  ( oppR ` ( Scalar ` W ) ) = ( oppR ` ( Scalar ` W ) )
12 eqid 
 |-  ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) = ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) )
13 5 6 7 1 2 8 9 10 11 12 4 ldualset 
 |-  ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` W ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) >. } ) )
14 13 fveq2d 
 |-  ( ph -> ( Base ` D ) = ( Base ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` W ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) >. } ) ) )
15 1 fvexi 
 |-  F e. _V
16 eqid 
 |-  ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` W ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) >. } ) = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` W ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) >. } )
17 16 lmodbase 
 |-  ( F e. _V -> F = ( Base ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` W ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) >. } ) ) )
18 15 17 ax-mp 
 |-  F = ( Base ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` W ) ) |` ( F X. F ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` W ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` W ) ) , f e. F |-> ( f oF ( .r ` ( Scalar ` W ) ) ( ( Base ` W ) X. { k } ) ) ) >. } ) )
19 14 3 18 3eqtr4g 
 |-  ( ph -> V = F )