Metamath Proof Explorer

Definition df-ldual

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 oF ( +gv ) allows it to be a set; see ofmres . 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)

Ref Expression
Assertion df-ldual ⊢ LDual = v ∈ V ⟼ Base ndx LFnl ⁡ v + ndx ∘ f ⁡ + Scalar ⁡ v ↾ LFnl ⁡ v × LFnl ⁡ v Scalar ⁡ ndx opp r ⁡ Scalar ⁡ v ∪ ⋅ ndx k ∈ Base Scalar ⁡ v , f ∈ LFnl ⁡ v ⟼ f ⋅ Scalar ⁡ v f Base v × k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cld class LDual
1 vv setvar v
2 cvv class V
3 cbs class Base
4 cnx class ndx
5 4 3 cfv class Base ndx
6 clfn class LFnl
7 1 cv setvar v
8 7 6 cfv class LFnl ⁡ v
9 5 8 cop class Base ndx LFnl ⁡ v
10 cplusg class + 𝑔
11 4 10 cfv class + ndx
12 csca class Scalar
13 7 12 cfv class Scalar ⁡ v
14 13 10 cfv class + Scalar ⁡ v
15 14 cof class ∘ f ⁡ + Scalar ⁡ v
16 8 8 cxp class LFnl ⁡ v × LFnl ⁡ v
17 15 16 cres class ∘ f ⁡ + Scalar ⁡ v ↾ LFnl ⁡ v × LFnl ⁡ v
18 11 17 cop class + ndx ∘ f ⁡ + Scalar ⁡ v ↾ LFnl ⁡ v × LFnl ⁡ v
19 4 12 cfv class Scalar ⁡ ndx
20 coppr class opp r
21 13 20 cfv class opp r ⁡ Scalar ⁡ v
22 19 21 cop class Scalar ⁡ ndx opp r ⁡ Scalar ⁡ v
23 9 18 22 ctp class Base ndx LFnl ⁡ v + ndx ∘ f ⁡ + Scalar ⁡ v ↾ LFnl ⁡ v × LFnl ⁡ v Scalar ⁡ ndx opp r ⁡ Scalar ⁡ v
24 cvsca class ⋅ 𝑠
25 4 24 cfv class ⋅ ndx
26 vk setvar k
27 13 3 cfv class Base Scalar ⁡ v
28 vf setvar f
29 28 cv setvar f
30 cmulr class ⋅ 𝑟
31 13 30 cfv class ⋅ Scalar ⁡ v
32 31 cof class ∘ f ⁡ ⋅ Scalar ⁡ v
33 7 3 cfv class Base v
34 26 cv setvar k
35 34 csn class k
36 33 35 cxp class Base v × k
37 29 36 32 co class f ⋅ Scalar ⁡ v f Base v × k
38 26 28 27 8 37 cmpo class k ∈ Base Scalar ⁡ v , f ∈ LFnl ⁡ v ⟼ f ⋅ Scalar ⁡ v f Base v × k
39 25 38 cop class ⋅ ndx k ∈ Base Scalar ⁡ v , f ∈ LFnl ⁡ v ⟼ f ⋅ Scalar ⁡ v f Base v × k
40 39 csn class ⋅ ndx k ∈ Base Scalar ⁡ v , f ∈ LFnl ⁡ v ⟼ f ⋅ Scalar ⁡ v f Base v × k
41 23 40 cun class Base ndx LFnl ⁡ v + ndx ∘ f ⁡ + Scalar ⁡ v ↾ LFnl ⁡ v × LFnl ⁡ v Scalar ⁡ ndx opp r ⁡ Scalar ⁡ v ∪ ⋅ ndx k ∈ Base Scalar ⁡ v , f ∈ LFnl ⁡ v ⟼ f ⋅ Scalar ⁡ v f Base v × k
42 1 2 41 cmpt class v ∈ V ⟼ Base ndx LFnl ⁡ v + ndx ∘ f ⁡ + Scalar ⁡ v ↾ LFnl ⁡ v × LFnl ⁡ v Scalar ⁡ ndx opp r ⁡ Scalar ⁡ v ∪ ⋅ ndx k ∈ Base Scalar ⁡ v , f ∈ LFnl ⁡ v ⟼ f ⋅ Scalar ⁡ v f Base v × k
43 0 42 wceq wff LDual = v ∈ V ⟼ Base ndx LFnl ⁡ v + ndx ∘ f ⁡ + Scalar ⁡ v ↾ LFnl ⁡ v × LFnl ⁡ v Scalar ⁡ ndx opp r ⁡ Scalar ⁡ v ∪ ⋅ ndx k ∈ Base Scalar ⁡ v , f ∈ LFnl ⁡ v ⟼ f ⋅ Scalar ⁡ v f Base v × k