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

Definition df-ldual 32761
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 6808. 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 32760 . 2  class LDual
2 vv . . 3  setvar  v
3 cvv 3031 . . 3  class  _V
4 cnx 15196 . . . . . . 7  class  ndx
5 cbs 15199 . . . . . . 7  class  Base
64, 5cfv 5589 . . . . . 6  class  ( Base `  ndx )
72cv 1451 . . . . . . 7  class  v
8 clfn 32694 . . . . . . 7  class LFnl
97, 8cfv 5589 . . . . . 6  class  (LFnl `  v )
106, 9cop 3965 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 15268 . . . . . . 7  class  +g
124, 11cfv 5589 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 15271 . . . . . . . . . 10  class Scalar
147, 13cfv 5589 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 5589 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6548 . . . . . . 7  class  oF ( +g  `  (Scalar `  v ) )
179, 9cxp 4837 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4841 . . . . . 6  class  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 3965 . . . . 5  class  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 5589 . . . . . 6  class  (Scalar `  ndx )
21 coppr 17928 . . . . . . 7  class oppr
2214, 21cfv 5589 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 3965 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 3963 . . . 4  class  { <. (
Base `  ndx ) ,  (LFnl `  v ) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }
25 cvsca 15272 . . . . . . 7  class  .s
264, 25cfv 5589 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  setvar  k
28 vf . . . . . . 7  setvar  f
2914, 5cfv 5589 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1451 . . . . . . . 8  class  f
317, 5cfv 5589 . . . . . . . . 9  class  ( Base `  v )
3227cv 1451 . . . . . . . . . 10  class  k
3332csn 3959 . . . . . . . . 9  class  { k }
3431, 33cxp 4837 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 15269 . . . . . . . . . 10  class  .r
3614, 35cfv 5589 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6548 . . . . . . . 8  class  oF ( .r `  (Scalar `  v ) )
3830, 34, 37co 6308 . . . . . . 7  class  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 6310 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 3965 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  oF ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 3959 . . . 4  class  { <. ( .s `  ndx ) ,  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) ) >. }
4224, 41cun 3388 . . 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 4454 . 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 1452 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  32762
  Copyright terms: Public domain W3C validator