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

Definition df-ldual 28581
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 6077. 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 28580 . 2  class LDual
2 vv . . 3  set  v
3 cvv 2789 . . 3  class  _V
4 cnx 13139 . . . . . . 7  class  ndx
5 cbs 13142 . . . . . . 7  class  Base
64, 5cfv 5221 . . . . . 6  class  ( Base `  ndx )
72cv 1623 . . . . . . 7  class  v
8 clfn 28514 . . . . . . 7  class LFnl
97, 8cfv 5221 . . . . . 6  class  (LFnl `  v )
106, 9cop 3644 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 13202 . . . . . . 7  class  +g
124, 11cfv 5221 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 13205 . . . . . . . . . 10  class Scalar
147, 13cfv 5221 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 5221 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6037 . . . . . . 7  class  o F ( +g  `  (Scalar `  v ) )
179, 9cxp 4686 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4690 . . . . . 6  class  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 3644 . . . . 5  class  <. ( +g  `  ndx ) ,  (  o F ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 5221 . . . . . 6  class  (Scalar `  ndx )
21 coppr 15398 . . . . . . 7  class oppr
2214, 21cfv 5221 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 3644 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 3643 . . . 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 13206 . . . . . . 7  class  .s
264, 25cfv 5221 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  set  k
28 vf . . . . . . 7  set  f
2914, 5cfv 5221 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1623 . . . . . . . 8  class  f
317, 5cfv 5221 . . . . . . . . 9  class  ( Base `  v )
3227cv 1623 . . . . . . . . . 10  class  k
3332csn 3641 . . . . . . . . 9  class  { k }
3431, 33cxp 4686 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 13203 . . . . . . . . . 10  class  .r
3614, 35cfv 5221 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6037 . . . . . . . 8  class  o F ( .r `  (Scalar `  v ) )
3830, 34, 37co 5819 . . . . . . 7  class  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 5821 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  o F ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 3644 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  o F ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 3641 . . . 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 3151 . . 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 4078 . 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 1624 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  28582
  Copyright terms: Public domain W3C validator