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

Definition df-ldual 36306
 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 ∘f (+g‘𝑣) allows it to be a set; see ofmres 7660. 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 ↦ ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}))
Distinct variable group:   𝑣,𝑘,𝑓

Detailed syntax breakdown of Definition df-ldual
StepHypRef Expression
1 cld 36305 . 2 class LDual
2 vv . . 3 setvar 𝑣
3 cvv 3471 . . 3 class V
4 cnx 16459 . . . . . . 7 class ndx
5 cbs 16462 . . . . . . 7 class Base
64, 5cfv 6328 . . . . . 6 class (Base‘ndx)
72cv 1537 . . . . . . 7 class 𝑣
8 clfn 36239 . . . . . . 7 class LFnl
97, 8cfv 6328 . . . . . 6 class (LFnl‘𝑣)
106, 9cop 4546 . . . . 5 class ⟨(Base‘ndx), (LFnl‘𝑣)⟩
11 cplusg 16544 . . . . . . 7 class +g
124, 11cfv 6328 . . . . . 6 class (+g‘ndx)
13 csca 16547 . . . . . . . . . 10 class Scalar
147, 13cfv 6328 . . . . . . . . 9 class (Scalar‘𝑣)
1514, 11cfv 6328 . . . . . . . 8 class (+g‘(Scalar‘𝑣))
1615cof 7382 . . . . . . 7 class f (+g‘(Scalar‘𝑣))
179, 9cxp 5526 . . . . . . 7 class ((LFnl‘𝑣) × (LFnl‘𝑣))
1816, 17cres 5530 . . . . . 6 class ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))
1912, 18cop 4546 . . . . 5 class ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩
204, 13cfv 6328 . . . . . 6 class (Scalar‘ndx)
21 coppr 19351 . . . . . . 7 class oppr
2214, 21cfv 6328 . . . . . 6 class (oppr‘(Scalar‘𝑣))
2320, 22cop 4546 . . . . 5 class ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩
2410, 19, 23ctp 4544 . . . 4 class {⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩}
25 cvsca 16548 . . . . . . 7 class ·𝑠
264, 25cfv 6328 . . . . . 6 class ( ·𝑠 ‘ndx)
27 vk . . . . . . 7 setvar 𝑘
28 vf . . . . . . 7 setvar 𝑓
2914, 5cfv 6328 . . . . . . 7 class (Base‘(Scalar‘𝑣))
3028cv 1537 . . . . . . . 8 class 𝑓
317, 5cfv 6328 . . . . . . . . 9 class (Base‘𝑣)
3227cv 1537 . . . . . . . . . 10 class 𝑘
3332csn 4540 . . . . . . . . 9 class {𝑘}
3431, 33cxp 5526 . . . . . . . 8 class ((Base‘𝑣) × {𝑘})
35 cmulr 16545 . . . . . . . . . 10 class .r
3614, 35cfv 6328 . . . . . . . . 9 class (.r‘(Scalar‘𝑣))
3736cof 7382 . . . . . . . 8 class f (.r‘(Scalar‘𝑣))
3830, 34, 37co 7130 . . . . . . 7 class (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘}))
3927, 28, 29, 9, 38cmpo 7132 . . . . . 6 class (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))
4026, 39cop 4546 . . . . 5 class ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩
4140csn 4540 . . . 4 class {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}
4224, 41cun 3908 . . 3 class ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩})
432, 3, 42cmpt 5119 . 2 class (𝑣 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}))
441, 43wceq 1538 1 wff LDual = (𝑣 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  ldualset  36307
 Copyright terms: Public domain W3C validator