Metamath Proof Explorer

Theorem ldualset

Description: Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in Holland95 p. 218. This allows us to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppR ring, for convenience. (Contributed by NM, 18-Oct-2014)

Ref Expression
Hypotheses ldualset.v 
|- V = ( Base ` W )
ldualset.a 
|- .+ = ( +g ` R )
ldualset.p 
|- .+b = ( oF .+ |` ( F X. F ) )
ldualset.f 
|- F = ( LFnl ` W )
ldualset.d 
|- D = ( LDual ` W )
ldualset.r 
|- R = ( Scalar ` W )
ldualset.k 
|- K = ( Base ` R )
ldualset.t 
|- .x. = ( .r ` R )
ldualset.o 
|- O = ( oppR ` R )
ldualset.s 
|- .xb = ( k e. K , f e. F |-> ( f oF .x. ( V X. { k } ) ) )
ldualset.w 
|- ( ph -> W e. X )
Assertion ldualset 
|- ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )

Proof

Step Hyp Ref Expression
1 ldualset.v 
 |-  V = ( Base ` W )
2 ldualset.a 
 |-  .+ = ( +g ` R )
3 ldualset.p 
 |-  .+b = ( oF .+ |` ( F X. F ) )
4 ldualset.f 
 |-  F = ( LFnl ` W )
5 ldualset.d 
 |-  D = ( LDual ` W )
6 ldualset.r 
 |-  R = ( Scalar ` W )
7 ldualset.k 
 |-  K = ( Base ` R )
8 ldualset.t 
 |-  .x. = ( .r ` R )
9 ldualset.o 
 |-  O = ( oppR ` R )
10 ldualset.s 
 |-  .xb = ( k e. K , f e. F |-> ( f oF .x. ( V X. { k } ) ) )
11 ldualset.w 
 |-  ( ph -> W e. X )
12 elex 
 |-  ( W e. X -> W e. _V )
13 fveq2 
 |-  ( w = W -> ( LFnl ` w ) = ( LFnl ` W ) )
14 13 4 eqtr4di 
 |-  ( w = W -> ( LFnl ` w ) = F )
15 14 opeq2d 
 |-  ( w = W -> <. ( Base ` ndx ) , ( LFnl ` w ) >. = <. ( Base ` ndx ) , F >. )
16 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
17 16 6 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = R )
18 17 fveq2d 
 |-  ( w = W -> ( +g ` ( Scalar ` w ) ) = ( +g ` R ) )
19 18 2 eqtr4di 
 |-  ( w = W -> ( +g ` ( Scalar ` w ) ) = .+ )
20 19 ofeqd 
 |-  ( w = W -> oF ( +g ` ( Scalar ` w ) ) = oF .+ )
21 14 sqxpeqd 
 |-  ( w = W -> ( ( LFnl ` w ) X. ( LFnl ` w ) ) = ( F X. F ) )
22 20 21 reseq12d 
 |-  ( w = W -> ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) = ( oF .+ |` ( F X. F ) ) )
23 22 3 eqtr4di 
 |-  ( w = W -> ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) = .+b )
24 23 opeq2d 
 |-  ( w = W -> <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) >. = <. ( +g ` ndx ) , .+b >. )
25 17 fveq2d 
 |-  ( w = W -> ( oppR ` ( Scalar ` w ) ) = ( oppR ` R ) )
26 25 9 eqtr4di 
 |-  ( w = W -> ( oppR ` ( Scalar ` w ) ) = O )
27 26 opeq2d 
 |-  ( w = W -> <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` w ) ) >. = <. ( Scalar ` ndx ) , O >. )
28 15 24 27 tpeq123d 
 |-  ( w = W -> { <. ( Base ` ndx ) , ( LFnl ` w ) >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` w ) ) >. } = { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } )
29 17 fveq2d 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = ( Base ` R ) )
30 29 7 eqtr4di 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = K )
31 17 fveq2d 
 |-  ( w = W -> ( .r ` ( Scalar ` w ) ) = ( .r ` R ) )
32 31 8 eqtr4di 
 |-  ( w = W -> ( .r ` ( Scalar ` w ) ) = .x. )
33 32 ofeqd 
 |-  ( w = W -> oF ( .r ` ( Scalar ` w ) ) = oF .x. )
34 eqidd 
 |-  ( w = W -> f = f )
35 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
36 35 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
37 36 xpeq1d 
 |-  ( w = W -> ( ( Base ` w ) X. { k } ) = ( V X. { k } ) )
38 33 34 37 oveq123d 
 |-  ( w = W -> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) = ( f oF .x. ( V X. { k } ) ) )
39 30 14 38 mpoeq123dv 
 |-  ( w = W -> ( k e. ( Base ` ( Scalar ` w ) ) , f e. ( LFnl ` w ) |-> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) ) = ( k e. K , f e. F |-> ( f oF .x. ( V X. { k } ) ) ) )
40 39 10 eqtr4di 
 |-  ( w = W -> ( k e. ( Base ` ( Scalar ` w ) ) , f e. ( LFnl ` w ) |-> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) ) = .xb )
41 40 opeq2d 
 |-  ( w = W -> <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` w ) ) , f e. ( LFnl ` w ) |-> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) ) >. = <. ( .s ` ndx ) , .xb >. )
42 41 sneqd 
 |-  ( w = W -> { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` w ) ) , f e. ( LFnl ` w ) |-> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) ) >. } = { <. ( .s ` ndx ) , .xb >. } )
43 28 42 uneq12d 
 |-  ( w = W -> ( { <. ( Base ` ndx ) , ( LFnl ` w ) >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` w ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` w ) ) , f e. ( LFnl ` w ) |-> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) ) >. } ) = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )
44 df-ldual 
 |-  LDual = ( w e. _V |-> ( { <. ( Base ` ndx ) , ( LFnl ` w ) >. , <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) >. , <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` w ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` ( Scalar ` w ) ) , f e. ( LFnl ` w ) |-> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) ) >. } ) )
45 tpex 
 |-  { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } e. _V
46 snex 
 |-  { <. ( .s ` ndx ) , .xb >. } e. _V
47 45 46 unex 
 |-  ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) e. _V
48 43 44 47 fvmpt 
 |-  ( W e. _V -> ( LDual ` W ) = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )
49 5 48 eqtrid 
 |-  ( W e. _V -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )
50 11 12 49 3syl 
 |-  ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )