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 33798
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 6772. 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 33797 . 2  class LDual
2 vv . . 3  setvar  v
3 cvv 3108 . . 3  class  _V
4 cnx 14478 . . . . . . 7  class  ndx
5 cbs 14481 . . . . . . 7  class  Base
64, 5cfv 5581 . . . . . 6  class  ( Base `  ndx )
72cv 1373 . . . . . . 7  class  v
8 clfn 33731 . . . . . . 7  class LFnl
97, 8cfv 5581 . . . . . 6  class  (LFnl `  v )
106, 9cop 4028 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 14546 . . . . . . 7  class  +g
124, 11cfv 5581 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 14549 . . . . . . . . . 10  class Scalar
147, 13cfv 5581 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 5581 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6515 . . . . . . 7  class  oF ( +g  `  (Scalar `  v ) )
179, 9cxp 4992 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4996 . . . . . 6  class  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 4028 . . . . 5  class  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 5581 . . . . . 6  class  (Scalar `  ndx )
21 coppr 17050 . . . . . . 7  class oppr
2214, 21cfv 5581 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 4028 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 4026 . . . 4  class  { <. (
Base `  ndx ) ,  (LFnl `  v ) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }
25 cvsca 14550 . . . . . . 7  class  .s
264, 25cfv 5581 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  setvar  k
28 vf . . . . . . 7  setvar  f
2914, 5cfv 5581 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1373 . . . . . . . 8  class  f
317, 5cfv 5581 . . . . . . . . 9  class  ( Base `  v )
3227cv 1373 . . . . . . . . . 10  class  k
3332csn 4022 . . . . . . . . 9  class  { k }
3431, 33cxp 4992 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 14547 . . . . . . . . . 10  class  .r
3614, 35cfv 5581 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6515 . . . . . . . 8  class  oF ( .r `  (Scalar `  v ) )
3830, 34, 37co 6277 . . . . . . 7  class  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 6279 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 4028 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  oF ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 4022 . . . 4  class  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. }
4224, 41cun 3469 . . 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 4500 . 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 1374 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  33799
  Copyright terms: Public domain W3C validator