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 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 LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-ldual
StepHypRef Expression
1 cld 32760 . 2 LDual
2 vv . . 3
3 cvv 3031 . . 3
4 cnx 15196 . . . . . . 7
5 cbs 15199 . . . . . . 7
64, 5cfv 5589 . . . . . 6
72cv 1451 . . . . . . 7
8 clfn 32694 . . . . . . 7 LFnl
97, 8cfv 5589 . . . . . 6 LFnl
106, 9cop 3965 . . . . 5 LFnl
11 cplusg 15268 . . . . . . 7
124, 11cfv 5589 . . . . . 6
13 csca 15271 . . . . . . . . . 10 Scalar
147, 13cfv 5589 . . . . . . . . 9 Scalar
1514, 11cfv 5589 . . . . . . . 8 Scalar
1615cof 6548 . . . . . . 7 Scalar
179, 9cxp 4837 . . . . . . 7 LFnl LFnl
1816, 17cres 4841 . . . . . 6 Scalar LFnl LFnl
1912, 18cop 3965 . . . . 5 Scalar LFnl LFnl
204, 13cfv 5589 . . . . . 6 Scalar
21 coppr 17928 . . . . . . 7 oppr
2214, 21cfv 5589 . . . . . 6 opprScalar
2320, 22cop 3965 . . . . 5 Scalar opprScalar
2410, 19, 23ctp 3963 . . . 4 LFnl Scalar LFnl LFnl Scalar opprScalar
25 cvsca 15272 . . . . . . 7
264, 25cfv 5589 . . . . . 6
27 vk . . . . . . 7
28 vf . . . . . . 7
2914, 5cfv 5589 . . . . . . 7 Scalar
3028cv 1451 . . . . . . . 8
317, 5cfv 5589 . . . . . . . . 9
3227cv 1451 . . . . . . . . . 10
3332csn 3959 . . . . . . . . 9
3431, 33cxp 4837 . . . . . . . 8
35 cmulr 15269 . . . . . . . . . 10
3614, 35cfv 5589 . . . . . . . . 9 Scalar
3736cof 6548 . . . . . . . 8 Scalar
3830, 34, 37co 6308 . . . . . . 7 Scalar
3927, 28, 29, 9, 38cmpt2 6310 . . . . . 6 Scalar LFnl Scalar
4026, 39cop 3965 . . . . 5 Scalar LFnl Scalar
4140csn 3959 . . . 4 Scalar LFnl Scalar
4224, 41cun 3388 . . 3 LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar
432, 3, 42cmpt 4454 . 2 LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar
441, 43wceq 1452 1 LDual LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar
 Colors of variables: wff setvar class This definition is referenced by:  ldualset  32762
 Copyright terms: Public domain W3C validator