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

Definition df-ldual 29761
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 6334. 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 29760 . 2  class LDual
2 vv . . 3  set  v
3 cvv 2948 . . 3  class  _V
4 cnx 13454 . . . . . . 7  class  ndx
5 cbs 13457 . . . . . . 7  class  Base
64, 5cfv 5445 . . . . . 6  class  ( Base `  ndx )
72cv 1651 . . . . . . 7  class  v
8 clfn 29694 . . . . . . 7  class LFnl
97, 8cfv 5445 . . . . . 6  class  (LFnl `  v )
106, 9cop 3809 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 13517 . . . . . . 7  class  +g
124, 11cfv 5445 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 13520 . . . . . . . . . 10  class Scalar
147, 13cfv 5445 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 5445 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6294 . . . . . . 7  class  o F ( +g  `  (Scalar `  v ) )
179, 9cxp 4867 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4871 . . . . . 6  class  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 3809 . . . . 5  class  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 5445 . . . . . 6  class  (Scalar `  ndx )
21 coppr 15715 . . . . . . 7  class oppr
2214, 21cfv 5445 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 3809 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 3808 . . . 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 13521 . . . . . . 7  class  .s
264, 25cfv 5445 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  set  k
28 vf . . . . . . 7  set  f
2914, 5cfv 5445 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1651 . . . . . . . 8  class  f
317, 5cfv 5445 . . . . . . . . 9  class  ( Base `  v )
3227cv 1651 . . . . . . . . . 10  class  k
3332csn 3806 . . . . . . . . 9  class  { k }
3431, 33cxp 4867 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 13518 . . . . . . . . . 10  class  .r
3614, 35cfv 5445 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6294 . . . . . . . 8  class  o F ( .r `  (Scalar `  v ) )
3830, 34, 37co 6072 . . . . . . 7  class  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 6074 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 3809 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  o F ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 3806 . . . 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 3310 . . 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 4258 . 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 1652 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  29762
  Copyright terms: Public domain W3C validator