Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ldual Unicode version

Definition df-ldual 28444
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. The restriction on  o F ( +g  `  v
) allows it to be a set; see ofmres 6015. 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.)
Assertion
Ref Expression
df-ldual  |- LDual  =  ( v  e.  _V  |->  ( { <. ( Base `  ndx ) ,  (LFnl `  v
) >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }  u.  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } ) )
Distinct variable group:    v, k, f

Detailed syntax breakdown of Definition df-ldual
StepHypRef Expression
1 cld 28443 . 2  class LDual
2 vv . . 3  set  v
3 cvv 2740 . . 3  class  _V
4 cnx 13072 . . . . . . 7  class  ndx
5 cbs 13075 . . . . . . 7  class  Base
64, 5cfv 4638 . . . . . 6  class  ( Base `  ndx )
72cv 1618 . . . . . . 7  class  v
8 clfn 28377 . . . . . . 7  class LFnl
97, 8cfv 4638 . . . . . 6  class  (LFnl `  v )
106, 9cop 3584 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 13135 . . . . . . 7  class  +g
124, 11cfv 4638 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 13138 . . . . . . . . . 10  class Scalar
147, 13cfv 4638 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 4638 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 5975 . . . . . . 7  class  o F ( +g  `  (Scalar `  v ) )
179, 9cxp 4624 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4628 . . . . . 6  class  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 3584 . . . . 5  class  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 4638 . . . . . 6  class  (Scalar `  ndx )
21 coppr 15331 . . . . . . 7  class oppr
2214, 21cfv 4638 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 3584 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 3583 . . . 4  class  { <. (
Base `  ndx ) ,  (LFnl `  v ) >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }
25 cvsca 13139 . . . . . . 7  class  .s
264, 25cfv 4638 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  set  k
28 vf . . . . . . 7  set  f
2914, 5cfv 4638 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1618 . . . . . . . 8  class  f
317, 5cfv 4638 . . . . . . . . 9  class  ( Base `  v )
3227cv 1618 . . . . . . . . . 10  class  k
3332csn 3581 . . . . . . . . 9  class  { k }
3431, 33cxp 4624 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 13136 . . . . . . . . . 10  class  .r
3614, 35cfv 4638 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 5975 . . . . . . . 8  class  o F ( .r `  (Scalar `  v ) )
3830, 34, 37co 5757 . . . . . . 7  class  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 5759 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 3584 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  o F ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 3581 . . . 4  class  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. }
4224, 41cun 3092 . . 3  class  ( {
<. ( Base `  ndx ) ,  (LFnl `  v
) >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }  u.  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } )
432, 3, 42cmpt 4017 . 2  class  ( v  e.  _V  |->  ( {
<. ( Base `  ndx ) ,  (LFnl `  v
) >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }  u.  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } ) )
441, 43wceq 1619 1  wff LDual  =  ( v  e.  _V  |->  ( { <. ( Base `  ndx ) ,  (LFnl `  v
) >. ,  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }  u.  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } ) )
Colors of variables: wff set class
This definition is referenced by:  ldualset  28445
  Copyright terms: Public domain W3C validator