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 34589
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 6781. 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 34588 . 2  class LDual
2 vv . . 3  setvar  v
3 cvv 3095 . . 3  class  _V
4 cnx 14506 . . . . . . 7  class  ndx
5 cbs 14509 . . . . . . 7  class  Base
64, 5cfv 5578 . . . . . 6  class  ( Base `  ndx )
72cv 1382 . . . . . . 7  class  v
8 clfn 34522 . . . . . . 7  class LFnl
97, 8cfv 5578 . . . . . 6  class  (LFnl `  v )
106, 9cop 4020 . . . . 5  class  <. ( Base `  ndx ) ,  (LFnl `  v ) >.
11 cplusg 14574 . . . . . . 7  class  +g
124, 11cfv 5578 . . . . . 6  class  ( +g  ` 
ndx )
13 csca 14577 . . . . . . . . . 10  class Scalar
147, 13cfv 5578 . . . . . . . . 9  class  (Scalar `  v )
1514, 11cfv 5578 . . . . . . . 8  class  ( +g  `  (Scalar `  v )
)
1615cof 6523 . . . . . . 7  class  oF ( +g  `  (Scalar `  v ) )
179, 9cxp 4987 . . . . . . 7  class  ( (LFnl `  v )  X.  (LFnl `  v ) )
1816, 17cres 4991 . . . . . 6  class  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) )
1912, 18cop 4020 . . . . 5  class  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >.
204, 13cfv 5578 . . . . . 6  class  (Scalar `  ndx )
21 coppr 17145 . . . . . . 7  class oppr
2214, 21cfv 5578 . . . . . 6  class  (oppr `  (Scalar `  v ) )
2320, 22cop 4020 . . . . 5  class  <. (Scalar ` 
ndx ) ,  (oppr `  (Scalar `  v ) )
>.
2410, 19, 23ctp 4018 . . . 4  class  { <. (
Base `  ndx ) ,  (LFnl `  v ) >. ,  <. ( +g  `  ndx ) ,  (  oF ( +g  `  (Scalar `  v ) )  |`  ( (LFnl `  v )  X.  (LFnl `  v )
) ) >. ,  <. (Scalar `  ndx ) ,  (oppr `  (Scalar `  v ) )
>. }
25 cvsca 14578 . . . . . . 7  class  .s
264, 25cfv 5578 . . . . . 6  class  ( .s
`  ndx )
27 vk . . . . . . 7  setvar  k
28 vf . . . . . . 7  setvar  f
2914, 5cfv 5578 . . . . . . 7  class  ( Base `  (Scalar `  v )
)
3028cv 1382 . . . . . . . 8  class  f
317, 5cfv 5578 . . . . . . . . 9  class  ( Base `  v )
3227cv 1382 . . . . . . . . . 10  class  k
3332csn 4014 . . . . . . . . 9  class  { k }
3431, 33cxp 4987 . . . . . . . 8  class  ( (
Base `  v )  X.  { k } )
35 cmulr 14575 . . . . . . . . . 10  class  .r
3614, 35cfv 5578 . . . . . . . . 9  class  ( .r
`  (Scalar `  v )
)
3736cof 6523 . . . . . . . 8  class  oF ( .r `  (Scalar `  v ) )
3830, 34, 37co 6281 . . . . . . 7  class  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) )
3927, 28, 29, 9, 38cmpt2 6283 . . . . . 6  class  ( k  e.  ( Base `  (Scalar `  v ) ) ,  f  e.  (LFnl `  v )  |->  ( f  oF ( .r
`  (Scalar `  v )
) ( ( Base `  v )  X.  {
k } ) ) )
4026, 39cop 4020 . . . . 5  class  <. ( .s `  ndx ) ,  ( k  e.  (
Base `  (Scalar `  v
) ) ,  f  e.  (LFnl `  v
)  |->  ( f  oF ( .r `  (Scalar `  v ) ) ( ( Base `  v
)  X.  { k } ) ) )
>.
4140csn 4014 . . . 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 4495 . 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 1383 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  34590
  Copyright terms: Public domain W3C validator