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 33225
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 7032. 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 33224 . 2 class LDual
2 vv . . 3 setvar 𝑣
3 cvv 3172 . . 3 class V
4 cnx 15638 . . . . . . 7 class ndx
5 cbs 15641 . . . . . . 7 class Base
64, 5cfv 5790 . . . . . 6 class (Base‘ndx)
72cv 1473 . . . . . . 7 class 𝑣
8 clfn 33158 . . . . . . 7 class LFnl
97, 8cfv 5790 . . . . . 6 class (LFnl‘𝑣)
106, 9cop 4130 . . . . 5 class ⟨(Base‘ndx), (LFnl‘𝑣)⟩
11 cplusg 15714 . . . . . . 7 class +g
124, 11cfv 5790 . . . . . 6 class (+g‘ndx)
13 csca 15717 . . . . . . . . . 10 class Scalar
147, 13cfv 5790 . . . . . . . . 9 class (Scalar‘𝑣)
1514, 11cfv 5790 . . . . . . . 8 class (+g‘(Scalar‘𝑣))
1615cof 6770 . . . . . . 7 class 𝑓 (+g‘(Scalar‘𝑣))
179, 9cxp 5026 . . . . . . 7 class ((LFnl‘𝑣) × (LFnl‘𝑣))
1816, 17cres 5030 . . . . . 6 class ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))
1912, 18cop 4130 . . . . 5 class ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩
204, 13cfv 5790 . . . . . 6 class (Scalar‘ndx)
21 coppr 18391 . . . . . . 7 class oppr
2214, 21cfv 5790 . . . . . 6 class (oppr‘(Scalar‘𝑣))
2320, 22cop 4130 . . . . 5 class ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩
2410, 19, 23ctp 4128 . . . 4 class {⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩}
25 cvsca 15718 . . . . . . 7 class ·𝑠
264, 25cfv 5790 . . . . . 6 class ( ·𝑠 ‘ndx)
27 vk . . . . . . 7 setvar 𝑘
28 vf . . . . . . 7 setvar 𝑓
2914, 5cfv 5790 . . . . . . 7 class (Base‘(Scalar‘𝑣))
3028cv 1473 . . . . . . . 8 class 𝑓
317, 5cfv 5790 . . . . . . . . 9 class (Base‘𝑣)
3227cv 1473 . . . . . . . . . 10 class 𝑘
3332csn 4124 . . . . . . . . 9 class {𝑘}
3431, 33cxp 5026 . . . . . . . 8 class ((Base‘𝑣) × {𝑘})
35 cmulr 15715 . . . . . . . . . 10 class .r
3614, 35cfv 5790 . . . . . . . . 9 class (.r‘(Scalar‘𝑣))
3736cof 6770 . . . . . . . 8 class 𝑓 (.r‘(Scalar‘𝑣))
3830, 34, 37co 6527 . . . . . . 7 class (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘}))
3927, 28, 29, 9, 38cmpt2 6529 . . . . . 6 class (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))
4026, 39cop 4130 . . . . 5 class ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩
4140csn 4124 . . . 4 class {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}
4224, 41cun 3537 . . 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 4637 . 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 1474 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  33226
  Copyright terms: Public domain W3C validator