Metamath Proof Explorer

Theorem ldualfvadd

Description: Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses ldualvadd.f 
|- F = ( LFnl ` W )
ldualvadd.r 
|- R = ( Scalar ` W )
ldualvadd.a 
|- .+ = ( +g ` R )
ldualvadd.d 
|- D = ( LDual ` W )
ldualvadd.p 
|- .+b = ( +g ` D )
ldualvadd.w 
|- ( ph -> W e. X )
ldualfvadd.q 
|- .+^ = ( oF .+ |` ( F X. F ) )
Assertion ldualfvadd 
|- ( ph -> .+b = .+^ )

Proof

Step Hyp Ref Expression
1 ldualvadd.f 
 |-  F = ( LFnl ` W )
2 ldualvadd.r 
 |-  R = ( Scalar ` W )
3 ldualvadd.a 
 |-  .+ = ( +g ` R )
4 ldualvadd.d 
 |-  D = ( LDual ` W )
5 ldualvadd.p 
 |-  .+b = ( +g ` D )
6 ldualvadd.w 
 |-  ( ph -> W e. X )
7 ldualfvadd.q 
 |-  .+^ = ( oF .+ |` ( F X. F ) )
8 eqid 
 |-  ( Base ` W ) = ( Base ` W )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
12 eqid 
 |-  ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) ) = ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) )
13 8 3 7 1 4 2 9 10 11 12 6 ldualset 
 |-  ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+^ >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) ) >. } ) )
14 13 fveq2d 
 |-  ( ph -> ( +g ` D ) = ( +g ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+^ >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) ) >. } ) ) )
15 1 fvexi 
 |-  F e. _V
16 id 
 |-  ( F e. _V -> F e. _V )
17 16 16 ofmresex 
 |-  ( F e. _V -> ( oF .+ |` ( F X. F ) ) e. _V )
18 15 17 ax-mp 
 |-  ( oF .+ |` ( F X. F ) ) e. _V
19 7 18 eqeltri 
 |-  .+^ e. _V
20 eqid 
 |-  ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+^ >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) ) >. } ) = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+^ >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) ) >. } )
21 20 lmodplusg 
 |-  ( .+^ e. _V -> .+^ = ( +g ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+^ >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) ) >. } ) ) )
22 19 21 ax-mp 
 |-  .+^ = ( +g ` ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+^ >. , <. ( Scalar ` ndx ) , ( oppR ` R ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` R ) , f e. F |-> ( f oF ( .r ` R ) ( ( Base ` W ) X. { k } ) ) ) >. } ) )
23 14 5 22 3eqtr4g 
 |-  ( ph -> .+b = .+^ )