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

Definition df-ldual 28115
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 5968. 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 28114 . 2  class LDual
2 vv . . 3  set  v
3 cvv 2727 . . 3  class  _V
4 cnx 13019 . . . . . . 7  class  ndx
5 cbs 13022 . . . . . . 7  class  Base
64, 5cfv 4592 . . . . . 6  class  ( Base `  ndx )
72cv 1618 . . . . . . 7  class  v
8 clfn 28048 . . . . . . 7  class LFnl
97, 8cfv 4592 . . . . . 6  class  (LFnl `  v )
106, 9cop 3547 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 13082 . . . . . . 7  class  +g
124, 11cfv 4592 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 13085 . . . . . . . . . 10  class Scalar
147, 13cfv 4592 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 4592 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 5928 . . . . . . 7  class  o F ( +g  `  (Scalar `  v ) )
179, 9cxp 4578 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4582 . . . . . 6  class  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 3547 . . . . 5  class  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 4592 . . . . . 6  class  (Scalar `  ndx )
21 coppr 15239 . . . . . . 7  class oppr
2214, 21cfv 4592 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 3547 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 3546 . . . 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 13086 . . . . . . 7  class  .s
264, 25cfv 4592 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  set  k
28 vf . . . . . . 7  set  f
2914, 5cfv 4592 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1618 . . . . . . . 8  class  f
317, 5cfv 4592 . . . . . . . . 9  class  ( Base `  v )
3227cv 1618 . . . . . . . . . 10  class  k
3332csn 3544 . . . . . . . . 9  class  { k }
3431, 33cxp 4578 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 13083 . . . . . . . . . 10  class  .r
3614, 35cfv 4592 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 5928 . . . . . . . 8  class  o F ( .r `  (Scalar `  v ) )
3830, 34, 37co 5710 . . . . . . 7  class  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 5712 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 3547 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  o F ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 3544 . . . 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 3076 . . 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 3974 . 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  28116
  Copyright terms: Public domain W3C validator