Metamath Proof Explorer

Theorem ldualsca

Description: The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualsca.f 
|- F = ( Scalar ` W )
ldualsca.o 
|- O = ( oppR ` F )
ldualsca.d 
|- D = ( LDual ` W )
ldualsca.r 
|- R = ( Scalar ` D )
ldualsca.w 
|- ( ph -> W e. X )
Assertion ldualsca 
|- ( ph -> R = O )

Proof

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