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 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 to use the original scalar ring instead of the oppR ring, for convenience. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Assertion	df-ldual	$$⊢\mathrm{LDual}=\left(v\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(v\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(v\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)},f\in \mathrm{LFnl}\left(v\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cld	$$class\mathrm{LDual}$$
1		vv	$$setvarv$$
2		cvv	$$class\mathrm{V}$$
3		cbs	$$class\mathrm{Base}$$
4		cnx	$$class\mathrm{ndx}$$
5	4 3	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
6		clfn	$$class\mathrm{LFnl}$$
7	1	cv	$$setvarv$$
8	7 6	cfv	$$class\mathrm{LFnl}\left(v\right)$$
9	5 8	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(v\right)⟩$$
10		cplusg	$$class{+}_{𝑔}$$
11	4 10	cfv	$$class{+}_{\mathrm{ndx}}$$
12		csca	$$class\mathrm{Scalar}$$
13	7 12	cfv	$$class\mathrm{Scalar}\left(v\right)$$
14	13 10	cfv	$$class{+}_{\mathrm{Scalar}\left(v\right)}$$
15	14	cof	$$class{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}$$
16	8 8	cxp	$$class\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)$$
17	15 16	cres	$$class\left({{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)}\right)$$
18	11 17	cop	$$class⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)}⟩$$
19	4 12	cfv	$$class\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
20		coppr	$$class{opp}_r$$
21	13 20	cfv	$$class{opp}_r\left(\mathrm{Scalar}\left(v\right)\right)$$
22	19 21	cop	$$class⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(v\right)\right)⟩$$
23	9 18 22	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(v\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(v\right)\right)⟩\right\}$$
24		cvsca	$$class{\cdot }_{𝑠}$$
25	4 24	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
26		vk	$$setvark$$
27	13 3	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)}$$
28		vf	$$setvarf$$
29	28	cv	$$setvarf$$
30		cmulr	$$class{\cdot }_{𝑟}$$
31	13 30	cfv	$$class{\cdot }_{\mathrm{Scalar}\left(v\right)}$$
32	31	cof	$$class{\circ }_f{\cdot }_{\mathrm{Scalar}\left(v\right)}$$
33	7 3	cfv	$$class{\mathrm{Base}}_v$$
34	26	cv	$$setvark$$
35	34	csn	$$class\left\{k\right\}$$
36	33 35	cxp	$$class\left({\mathrm{Base}}_v\times \left\{k\right\}\right)$$
37	29 36 32	co	$$class\left(f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)$$
38	26 28 27 8 37	cmpo	$$class\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)},f\in \mathrm{LFnl}\left(v\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)$$
39	25 38	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)},f\in \mathrm{LFnl}\left(v\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)⟩$$
40	39	csn	$$class\left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)},f\in \mathrm{LFnl}\left(v\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)⟩\right\}$$
41	23 40	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(v\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(v\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)},f\in \mathrm{LFnl}\left(v\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)⟩\right\}\right)$$
42	1 2 41	cmpt	$$class\left(v\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(v\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(v\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)},f\in \mathrm{LFnl}\left(v\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)⟩\right\}\right)$$
43	0 42	wceq	$$wff\mathrm{LDual}=\left(v\in \mathrm{V}⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{LFnl}\left(v\right)⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f{+}_{\mathrm{Scalar}\left(v\right)}\upharpoonright }_{\left(\mathrm{LFnl}\left(v\right)\times \mathrm{LFnl}\left(v\right)\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{opp}_r\left(\mathrm{Scalar}\left(v\right)\right)⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(k\in {\mathrm{Base}}_{\mathrm{Scalar}\left(v\right)},f\in \mathrm{LFnl}\left(v\right)⟼f{{\cdot }_{\mathrm{Scalar}\left(v\right)}}_f\left({\mathrm{Base}}_v\times \left\{k\right\}\right)\right)⟩\right\}\right)$$