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

Definition df-ldual 28481
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 6050. 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 28480 . 2  class LDual
2 vv . . 3  set  v
3 cvv 2763 . . 3  class  _V
4 cnx 13107 . . . . . . 7  class  ndx
5 cbs 13110 . . . . . . 7  class  Base
64, 5cfv 4673 . . . . . 6  class  ( Base `  ndx )
72cv 1618 . . . . . . 7  class  v
8 clfn 28414 . . . . . . 7  class LFnl
97, 8cfv 4673 . . . . . 6  class  (LFnl `  v )
106, 9cop 3617 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 13170 . . . . . . 7  class  +g
124, 11cfv 4673 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 13173 . . . . . . . . . 10  class Scalar
147, 13cfv 4673 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 4673 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6010 . . . . . . 7  class  o F ( +g  `  (Scalar `  v ) )
179, 9cxp 4659 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4663 . . . . . 6  class  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 3617 . . . . 5  class  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 4673 . . . . . 6  class  (Scalar `  ndx )
21 coppr 15366 . . . . . . 7  class oppr
2214, 21cfv 4673 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 3617 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 3616 . . . 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 13174 . . . . . . 7  class  .s
264, 25cfv 4673 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  set  k
28 vf . . . . . . 7  set  f
2914, 5cfv 4673 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1618 . . . . . . . 8  class  f
317, 5cfv 4673 . . . . . . . . 9  class  ( Base `  v )
3227cv 1618 . . . . . . . . . 10  class  k
3332csn 3614 . . . . . . . . 9  class  { k }
3431, 33cxp 4659 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 13171 . . . . . . . . . 10  class  .r
3614, 35cfv 4673 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6010 . . . . . . . 8  class  o F ( .r `  (Scalar `  v ) )
3830, 34, 37co 5792 . . . . . . 7  class  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 5794 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 3617 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  o F ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 3614 . . . 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 3125 . . 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 4051 . 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  28482
  Copyright terms: Public domain W3C validator