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

Definition df-ldual 29314
 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 6116. 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 29313 . 2 LDual
2 vv . . 3
3 cvv 2788 . . 3
4 cnx 13145 . . . . . . 7
5 cbs 13148 . . . . . . 7
64, 5cfv 5255 . . . . . 6
72cv 1622 . . . . . . 7
8 clfn 29247 . . . . . . 7 LFnl
97, 8cfv 5255 . . . . . 6 LFnl
106, 9cop 3643 . . . . 5 LFnl
11 cplusg 13208 . . . . . . 7
124, 11cfv 5255 . . . . . 6
13 csca 13211 . . . . . . . . . 10 Scalar
147, 13cfv 5255 . . . . . . . . 9 Scalar
1514, 11cfv 5255 . . . . . . . 8 Scalar
1615cof 6076 . . . . . . 7 Scalar
179, 9cxp 4687 . . . . . . 7 LFnl LFnl
1816, 17cres 4691 . . . . . 6 Scalar LFnl LFnl
1912, 18cop 3643 . . . . 5 Scalar LFnl LFnl
204, 13cfv 5255 . . . . . 6 Scalar
21 coppr 15404 . . . . . . 7 oppr
2214, 21cfv 5255 . . . . . 6 opprScalar
2320, 22cop 3643 . . . . 5 Scalar opprScalar
2410, 19, 23ctp 3642 . . . 4 LFnl Scalar LFnl LFnl Scalar opprScalar
25 cvsca 13212 . . . . . . 7
264, 25cfv 5255 . . . . . 6
27 vk . . . . . . 7
28 vf . . . . . . 7
2914, 5cfv 5255 . . . . . . 7 Scalar
3028cv 1622 . . . . . . . 8
317, 5cfv 5255 . . . . . . . . 9
3227cv 1622 . . . . . . . . . 10
3332csn 3640 . . . . . . . . 9
3431, 33cxp 4687 . . . . . . . 8
35 cmulr 13209 . . . . . . . . . 10
3614, 35cfv 5255 . . . . . . . . 9 Scalar
3736cof 6076 . . . . . . . 8 Scalar
3830, 34, 37co 5858 . . . . . . 7 Scalar
3927, 28, 29, 9, 38cmpt2 5860 . . . . . 6 Scalar LFnl Scalar
4026, 39cop 3643 . . . . 5 Scalar LFnl Scalar
4140csn 3640 . . . 4 Scalar LFnl Scalar
4224, 41cun 3150 . . 3 LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar
432, 3, 42cmpt 4077 . 2 LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar
441, 43wceq 1623 1 LDual LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar
 Colors of variables: wff set class This definition is referenced by:  ldualset  29315
 Copyright terms: Public domain W3C validator