Definition df-ldual 36420

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 7667. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the opp_r 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

Step	Hyp	Ref	Expression
1		cld 36419	. 2 class LDual
2		vv	. . 3 setvar 𝑣
3		cvv 3441	. . 3 class V
4		cnx 16472	. . . . . . 7 class ndx
5		cbs 16475	. . . . . . 7 class Base
6	4, 5	cfv 6324	. . . . . 6 class (Base‘ndx)
7	2	cv 1537	. . . . . . 7 class 𝑣
8		clfn 36353	. . . . . . 7 class LFnl
9	7, 8	cfv 6324	. . . . . 6 class (LFnl‘𝑣)
10	6, 9	cop 4531	. . . . 5 class ⟨(Base‘ndx), (LFnl‘𝑣)⟩
11		cplusg 16557	. . . . . . 7 class +g
12	4, 11	cfv 6324	. . . . . 6 class (+g‘ndx)
13		csca 16560	. . . . . . . . . 10 class Scalar
14	7, 13	cfv 6324	. . . . . . . . 9 class (Scalar‘𝑣)
15	14, 11	cfv 6324	. . . . . . . 8 class (+g‘(Scalar‘𝑣))
16	15	cof 7387	. . . . . . 7 class ∘f (+g‘(Scalar‘𝑣))
17	9, 9	cxp 5517	. . . . . . 7 class ((LFnl‘𝑣) × (LFnl‘𝑣))
18	16, 17	cres 5521	. . . . . 6 class ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))
19	12, 18	cop 4531	. . . . 5 class ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩
20	4, 13	cfv 6324	. . . . . 6 class (Scalar‘ndx)
21		coppr 19368	. . . . . . 7 class oppr
22	14, 21	cfv 6324	. . . . . 6 class (oppr‘(Scalar‘𝑣))
23	20, 22	cop 4531	. . . . 5 class ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩
24	10, 19, 23	ctp 4529	. . . 4 class {⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩}
25		cvsca 16561	. . . . . . 7 class ·𝑠
26	4, 25	cfv 6324	. . . . . 6 class ( ·𝑠 ‘ndx)
27		vk	. . . . . . 7 setvar 𝑘
28		vf	. . . . . . 7 setvar 𝑓
29	14, 5	cfv 6324	. . . . . . 7 class (Base‘(Scalar‘𝑣))
30	28	cv 1537	. . . . . . . 8 class 𝑓
31	7, 5	cfv 6324	. . . . . . . . 9 class (Base‘𝑣)
32	27	cv 1537	. . . . . . . . . 10 class 𝑘
33	32	csn 4525	. . . . . . . . 9 class {𝑘}
34	31, 33	cxp 5517	. . . . . . . 8 class ((Base‘𝑣) × {𝑘})
35		cmulr 16558	. . . . . . . . . 10 class .r
36	14, 35	cfv 6324	. . . . . . . . 9 class (.r‘(Scalar‘𝑣))
37	36	cof 7387	. . . . . . . 8 class ∘f (.r‘(Scalar‘𝑣))
38	30, 34, 37	co 7135	. . . . . . 7 class (𝑓 ∘f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘}))
39	27, 28, 29, 9, 38	cmpo 7137	. . . . . 6 class (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))
40	26, 39	cop 4531	. . . . 5 class ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩
41	40	csn 4525	. . . 4 class {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩}
42	24, 41	cun 3879	. . 3 class ({⟨(Base‘ndx), (LFnl‘𝑣)⟩, ⟨(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))⟩, ⟨(Scalar‘ndx), (oppr‘(Scalar‘𝑣))⟩} ∪ {⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))⟩})
43	2, 3, 42	cmpt 5110	. 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‘𝑣) × {𝑘})))⟩}))
44	1, 43	wceq 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‘𝑣) × {𝑘})))⟩}))

This definition is referenced by:  ldualset  36421