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 ofeq 
 |-  ( ( +g ` ( Scalar ` w ) ) = .+ -> oF ( +g ` ( Scalar ` w ) ) = oF .+ )
21 19 20 syl 
 |-  ( w = W -> oF ( +g ` ( Scalar ` w ) ) = oF .+ )
22 14 sqxpeqd 
 |-  ( w = W -> ( ( LFnl ` w ) X. ( LFnl ` w ) ) = ( F X. F ) )
23 21 22 reseq12d 
 |-  ( w = W -> ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) = ( oF .+ |` ( F X. F ) ) )
24 23 3 eqtr4di 
 |-  ( w = W -> ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) = .+b )
25 24 opeq2d 
 |-  ( w = W -> <. ( +g ` ndx ) , ( oF ( +g ` ( Scalar ` w ) ) |` ( ( LFnl ` w ) X. ( LFnl ` w ) ) ) >. = <. ( +g ` ndx ) , .+b >. )
26 17 fveq2d 
 |-  ( w = W -> ( oppR ` ( Scalar ` w ) ) = ( oppR ` R ) )
27 26 9 eqtr4di 
 |-  ( w = W -> ( oppR ` ( Scalar ` w ) ) = O )
28 27 opeq2d 
 |-  ( w = W -> <. ( Scalar ` ndx ) , ( oppR ` ( Scalar ` w ) ) >. = <. ( Scalar ` ndx ) , O >. )
29 15 25 28 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 >. } )
30 17 fveq2d 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = ( Base ` R ) )
31 30 7 eqtr4di 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = K )
32 17 fveq2d 
 |-  ( w = W -> ( .r ` ( Scalar ` w ) ) = ( .r ` R ) )
33 32 8 eqtr4di 
 |-  ( w = W -> ( .r ` ( Scalar ` w ) ) = .x. )
34 ofeq 
 |-  ( ( .r ` ( Scalar ` w ) ) = .x. -> oF ( .r ` ( Scalar ` w ) ) = oF .x. )
35 33 34 syl 
 |-  ( w = W -> oF ( .r ` ( Scalar ` w ) ) = oF .x. )
36 eqidd 
 |-  ( w = W -> f = f )
37 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
38 37 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
39 38 xpeq1d 
 |-  ( w = W -> ( ( Base ` w ) X. { k } ) = ( V X. { k } ) )
40 35 36 39 oveq123d 
 |-  ( w = W -> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) = ( f oF .x. ( V X. { k } ) ) )
41 31 14 40 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 } ) ) ) )
42 41 10 eqtr4di 
 |-  ( w = W -> ( k e. ( Base ` ( Scalar ` w ) ) , f e. ( LFnl ` w ) |-> ( f oF ( .r ` ( Scalar ` w ) ) ( ( Base ` w ) X. { k } ) ) ) = .xb )
43 42 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 >. )
44 43 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 >. } )
45 29 44 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 >. } ) )
46 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 } ) ) ) >. } ) )
47 tpex 
 |-  { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } e. _V
48 snex 
 |-  { <. ( .s ` ndx ) , .xb >. } e. _V
49 47 48 unex 
 |-  ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) e. _V
50 45 46 49 fvmpt 
 |-  ( W e. _V -> ( LDual ` W ) = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )
51 5 50 syl5eq 
 |-  ( W e. _V -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )
52 11 12 51 3syl 
 |-  ( ph -> D = ( { <. ( Base ` ndx ) , F >. , <. ( +g ` ndx ) , .+b >. , <. ( Scalar ` ndx ) , O >. } u. { <. ( .s ` ndx ) , .xb >. } ) )