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

Detailed syntax breakdown of Definition df-ldual
StepHypRef Expression
1 cld 34925 . 2 class LDual
2 vv . . 3 setvar 𝑣
3 cvv 3349 . . 3 class V
4 cnx 16060 . . . . . . 7 class ndx
5 cbs 16063 . . . . . . 7 class Base
64, 5cfv 6031 . . . . . 6 class (Base‘ndx)
72cv 1629 . . . . . . 7 class 𝑣
8 clfn 34859 . . . . . . 7 class LFnl
97, 8cfv 6031 . . . . . 6 class (LFnl‘𝑣)
106, 9cop 4320 . . . . 5 class ⟨(Base‘ndx), (LFnl‘𝑣)⟩
11 cplusg 16148 . . . . . . 7 class +g
124, 11cfv 6031 . . . . . 6 class (+g‘ndx)
13 csca 16151 . . . . . . . . . 10 class Scalar
147, 13cfv 6031 . . . . . . . . 9 class (Scalar‘𝑣)
1514, 11cfv 6031 . . . . . . . 8 class (+g‘(Scalar‘𝑣))
1615cof 7041 . . . . . . 7 class 𝑓 (+g‘(Scalar‘𝑣))
179, 9cxp 5247 . . . . . . 7 class ((LFnl‘𝑣) × (LFnl‘𝑣))
1816, 17cres 5251 . . . . . 6 class ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))
1912, 18cop 4320 . . . . 5 class ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩
204, 13cfv 6031 . . . . . 6 class (Scalar‘ndx)
21 coppr 18829 . . . . . . 7 class oppr
2214, 21cfv 6031 . . . . . 6 class (oppr‘(Scalar‘𝑣))
2320, 22cop 4320 . . . . 5 class ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩
2410, 19, 23ctp 4318 . . . 4 class {⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩}
25 cvsca 16152 . . . . . . 7 class ·𝑠
264, 25cfv 6031 . . . . . 6 class ( ·𝑠 ‘ndx)
27 vk . . . . . . 7 setvar 𝑘
28 vf . . . . . . 7 setvar 𝑓
2914, 5cfv 6031 . . . . . . 7 class (Base‘(Scalar‘𝑣))
3028cv 1629 . . . . . . . 8 class 𝑓
317, 5cfv 6031 . . . . . . . . 9 class (Base‘𝑣)
3227cv 1629 . . . . . . . . . 10 class 𝑘
3332csn 4314 . . . . . . . . 9 class {𝑘}
3431, 33cxp 5247 . . . . . . . 8 class ((Base‘𝑣) × {𝑘})
35 cmulr 16149 . . . . . . . . . 10 class .r
3614, 35cfv 6031 . . . . . . . . 9 class (.r‘(Scalar‘𝑣))
3736cof 7041 . . . . . . . 8 class 𝑓 (.r‘(Scalar‘𝑣))
3830, 34, 37co 6792 . . . . . . 7 class (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘}))
3927, 28, 29, 9, 38cmpt2 6794 . . . . . 6 class (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))
4026, 39cop 4320 . . . . 5 class ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩
4140csn 4314 . . . 4 class {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}
4224, 41cun 3719 . . 3 class ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩})
432, 3, 42cmpt 4861 . 2 class (𝑣 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}))
441, 43wceq 1630 1 wff LDual = (𝑣 ∈ V ↦ ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  ldualset  34927
 Copyright terms: Public domain W3C validator