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 35136
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 7395. 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 35135 . 2 class LDual
2 vv . . 3 setvar 𝑣
3 cvv 3383 . . 3 class V
4 cnx 16177 . . . . . . 7 class ndx
5 cbs 16180 . . . . . . 7 class Base
64, 5cfv 6099 . . . . . 6 class (Base‘ndx)
72cv 1652 . . . . . . 7 class 𝑣
8 clfn 35069 . . . . . . 7 class LFnl
97, 8cfv 6099 . . . . . 6 class (LFnl‘𝑣)
106, 9cop 4372 . . . . 5 class ⟨(Base‘ndx), (LFnl‘𝑣)⟩
11 cplusg 16263 . . . . . . 7 class +g
124, 11cfv 6099 . . . . . 6 class (+g‘ndx)
13 csca 16266 . . . . . . . . . 10 class Scalar
147, 13cfv 6099 . . . . . . . . 9 class (Scalar‘𝑣)
1514, 11cfv 6099 . . . . . . . 8 class (+g‘(Scalar‘𝑣))
1615cof 7127 . . . . . . 7 class 𝑓 (+g‘(Scalar‘𝑣))
179, 9cxp 5308 . . . . . . 7 class ((LFnl‘𝑣) × (LFnl‘𝑣))
1816, 17cres 5312 . . . . . 6 class ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))
1912, 18cop 4372 . . . . 5 class ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩
204, 13cfv 6099 . . . . . 6 class (Scalar‘ndx)
21 coppr 18934 . . . . . . 7 class oppr
2214, 21cfv 6099 . . . . . 6 class (oppr‘(Scalar‘𝑣))
2320, 22cop 4372 . . . . 5 class ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩
2410, 19, 23ctp 4370 . . . 4 class {⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩}
25 cvsca 16267 . . . . . . 7 class ·𝑠
264, 25cfv 6099 . . . . . 6 class ( ·𝑠 ‘ndx)
27 vk . . . . . . 7 setvar 𝑘
28 vf . . . . . . 7 setvar 𝑓
2914, 5cfv 6099 . . . . . . 7 class (Base‘(Scalar‘𝑣))
3028cv 1652 . . . . . . . 8 class 𝑓
317, 5cfv 6099 . . . . . . . . 9 class (Base‘𝑣)
3227cv 1652 . . . . . . . . . 10 class 𝑘
3332csn 4366 . . . . . . . . 9 class {𝑘}
3431, 33cxp 5308 . . . . . . . 8 class ((Base‘𝑣) × {𝑘})
35 cmulr 16264 . . . . . . . . . 10 class .r
3614, 35cfv 6099 . . . . . . . . 9 class (.r‘(Scalar‘𝑣))
3736cof 7127 . . . . . . . 8 class 𝑓 (.r‘(Scalar‘𝑣))
3830, 34, 37co 6876 . . . . . . 7 class (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘}))
3927, 28, 29, 9, 38cmpt2 6878 . . . . . 6 class (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))
4026, 39cop 4372 . . . . 5 class ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩
4140csn 4366 . . . 4 class {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}
4224, 41cun 3765 . . 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 4920 . 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 1653 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  35137
  Copyright terms: Public domain W3C validator