Users' Mathboxes 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 34729
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 7206. 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 34728 . 2 class LDual
2 vv . . 3 setvar 𝑣
3 cvv 3231 . . 3 class V
4 cnx 15901 . . . . . . 7 class ndx
5 cbs 15904 . . . . . . 7 class Base
64, 5cfv 5926 . . . . . 6 class (Base‘ndx)
72cv 1522 . . . . . . 7 class 𝑣
8 clfn 34662 . . . . . . 7 class LFnl
97, 8cfv 5926 . . . . . 6 class (LFnl‘𝑣)
106, 9cop 4216 . . . . 5 class ⟨(Base‘ndx), (LFnl‘𝑣)⟩
11 cplusg 15988 . . . . . . 7 class +g
124, 11cfv 5926 . . . . . 6 class (+g‘ndx)
13 csca 15991 . . . . . . . . . 10 class Scalar
147, 13cfv 5926 . . . . . . . . 9 class (Scalar‘𝑣)
1514, 11cfv 5926 . . . . . . . 8 class (+g‘(Scalar‘𝑣))
1615cof 6937 . . . . . . 7 class 𝑓 (+g‘(Scalar‘𝑣))
179, 9cxp 5141 . . . . . . 7 class ((LFnl‘𝑣) × (LFnl‘𝑣))
1816, 17cres 5145 . . . . . 6 class ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))
1912, 18cop 4216 . . . . 5 class ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩
204, 13cfv 5926 . . . . . 6 class (Scalar‘ndx)
21 coppr 18668 . . . . . . 7 class oppr
2214, 21cfv 5926 . . . . . 6 class (oppr‘(Scalar‘𝑣))
2320, 22cop 4216 . . . . 5 class ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩
2410, 19, 23ctp 4214 . . . 4 class {⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩}
25 cvsca 15992 . . . . . . 7 class ·𝑠
264, 25cfv 5926 . . . . . 6 class ( ·𝑠 ‘ndx)
27 vk . . . . . . 7 setvar 𝑘
28 vf . . . . . . 7 setvar 𝑓
2914, 5cfv 5926 . . . . . . 7 class (Base‘(Scalar‘𝑣))
3028cv 1522 . . . . . . . 8 class 𝑓
317, 5cfv 5926 . . . . . . . . 9 class (Base‘𝑣)
3227cv 1522 . . . . . . . . . 10 class 𝑘
3332csn 4210 . . . . . . . . 9 class {𝑘}
3431, 33cxp 5141 . . . . . . . 8 class ((Base‘𝑣) × {𝑘})
35 cmulr 15989 . . . . . . . . . 10 class .r
3614, 35cfv 5926 . . . . . . . . 9 class (.r‘(Scalar‘𝑣))
3736cof 6937 . . . . . . . 8 class 𝑓 (.r‘(Scalar‘𝑣))
3830, 34, 37co 6690 . . . . . . 7 class (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘}))
3927, 28, 29, 9, 38cmpt2 6692 . . . . . 6 class (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))
4026, 39cop 4216 . . . . 5 class ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩
4140csn 4210 . . . 4 class {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}
4224, 41cun 3605 . . 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 4762 . 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 1523 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  34730
  Copyright terms: Public domain W3C validator