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 35246
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 6769. 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 35245 . 2  class LDual
2 vv . . 3  setvar  v
3 cvv 3106 . . 3  class  _V
4 cnx 14713 . . . . . . 7  class  ndx
5 cbs 14716 . . . . . . 7  class  Base
64, 5cfv 5570 . . . . . 6  class  ( Base `  ndx )
72cv 1397 . . . . . . 7  class  v
8 clfn 35179 . . . . . . 7  class LFnl
97, 8cfv 5570 . . . . . 6  class  (LFnl `  v )
106, 9cop 4022 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 14784 . . . . . . 7  class  +g
124, 11cfv 5570 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 14787 . . . . . . . . . 10  class Scalar
147, 13cfv 5570 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 5570 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6511 . . . . . . 7  class  oF ( +g  `  (Scalar `  v ) )
179, 9cxp 4986 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4990 . . . . . 6  class  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 4022 . . . . 5  class  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 5570 . . . . . 6  class  (Scalar `  ndx )
21 coppr 17466 . . . . . . 7  class oppr
2214, 21cfv 5570 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 4022 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 4020 . . . 4  class  { <. (
Base `  ndx ) ,  (LFnl `  v ) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }
25 cvsca 14788 . . . . . . 7  class  .s
264, 25cfv 5570 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  setvar  k
28 vf . . . . . . 7  setvar  f
2914, 5cfv 5570 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1397 . . . . . . . 8  class  f
317, 5cfv 5570 . . . . . . . . 9  class  ( Base `  v )
3227cv 1397 . . . . . . . . . 10  class  k
3332csn 4016 . . . . . . . . 9  class  { k }
3431, 33cxp 4986 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 14785 . . . . . . . . . 10  class  .r
3614, 35cfv 5570 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6511 . . . . . . . 8  class  oF ( .r `  (Scalar `  v ) )
3830, 34, 37co 6270 . . . . . . 7  class  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 6272 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 4022 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  oF ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 4016 . . . 4  class  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. }
4224, 41cun 3459 . . 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 4497 . 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 1398 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  35247
  Copyright terms: Public domain W3C validator