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

Definition df-ldual 33077
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  oF ( +g  `  v
) allows it to be a set; see ofmres 6675. 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 ) ,  (  oF ( +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  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } ) )
Distinct variable group:    v, k, f

Detailed syntax breakdown of Definition df-ldual
StepHypRef Expression
1 cld 33076 . 2  class LDual
2 vv . . 3  setvar  v
3 cvv 3070 . . 3  class  _V
4 cnx 14275 . . . . . . 7  class  ndx
5 cbs 14278 . . . . . . 7  class  Base
64, 5cfv 5518 . . . . . 6  class  ( Base `  ndx )
72cv 1369 . . . . . . 7  class  v
8 clfn 33010 . . . . . . 7  class LFnl
97, 8cfv 5518 . . . . . 6  class  (LFnl `  v )
106, 9cop 3983 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 14342 . . . . . . 7  class  +g
124, 11cfv 5518 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 14345 . . . . . . . . . 10  class Scalar
147, 13cfv 5518 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 5518 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6420 . . . . . . 7  class  oF ( +g  `  (Scalar `  v ) )
179, 9cxp 4938 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4942 . . . . . 6  class  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 3983 . . . . 5  class  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 5518 . . . . . 6  class  (Scalar `  ndx )
21 coppr 16822 . . . . . . 7  class oppr
2214, 21cfv 5518 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 3983 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 3981 . . . 4  class  { <. (
Base `  ndx ) ,  (LFnl `  v ) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }
25 cvsca 14346 . . . . . . 7  class  .s
264, 25cfv 5518 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  setvar  k
28 vf . . . . . . 7  setvar  f
2914, 5cfv 5518 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1369 . . . . . . . 8  class  f
317, 5cfv 5518 . . . . . . . . 9  class  ( Base `  v )
3227cv 1369 . . . . . . . . . 10  class  k
3332csn 3977 . . . . . . . . 9  class  { k }
3431, 33cxp 4938 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 14343 . . . . . . . . . 10  class  .r
3614, 35cfv 5518 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6420 . . . . . . . 8  class  oF ( .r `  (Scalar `  v ) )
3830, 34, 37co 6192 . . . . . . 7  class  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 6194 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 3983 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  oF ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 3977 . . . 4  class  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. }
4224, 41cun 3426 . . 3  class  ( {
<. ( Base `  ndx ) ,  (LFnl `  v
) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +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  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } )
432, 3, 42cmpt 4450 . 2  class  ( v  e.  _V  |->  ( {
<. ( Base `  ndx ) ,  (LFnl `  v
) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +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  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } ) )
441, 43wceq 1370 1  wff LDual  =  ( v  e.  _V  |->  ( { <. ( Base `  ndx ) ,  (LFnl `  v
) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +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  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. } ) )
Colors of variables: wff setvar class
This definition is referenced by:  ldualset  33078
  Copyright terms: Public domain W3C validator