Definition df-ldual 34589

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 ( +g ` v ) allows it to be a set; see ofmres 6781. 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 e. _V |-> ( { <. ( Base ` ndx ) , (LFnl ` v ) >. , <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >. , <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >. } ) )

Distinct variable group:   v, k, f

Detailed syntax breakdown of Definition df-ldual

Step	Hyp	Ref	Expression
1		cld 34588	. 2 class LDual
2		vv	. . 3 setvar v
3		cvv 3095	. . 3 class _V
4		cnx 14506	. . . . . . 7 class ndx
5		cbs 14509	. . . . . . 7 class Base
6	4, 5	cfv 5578	. . . . . 6 class ( Base ` ndx )
7	2	cv 1382	. . . . . . 7 class v
8		clfn 34522	. . . . . . 7 class LFnl
9	7, 8	cfv 5578	. . . . . 6 class (LFnl ` v )
10	6, 9	cop 4020	. . . . 5 class <. ( Base ` ndx ) , (LFnl ` v ) >.
11		cplusg 14574	. . . . . . 7 class +g
12	4, 11	cfv 5578	. . . . . 6 class ( +g ` ndx )
13		csca 14577	. . . . . . . . . 10 class Scalar
14	7, 13	cfv 5578	. . . . . . . . 9 class (Scalar ` v )
15	14, 11	cfv 5578	. . . . . . . 8 class ( +g ` (Scalar ` v ) )
16	15	cof 6523	. . . . . . 7 class oF ( +g ` (Scalar ` v ) )
17	9, 9	cxp 4987	. . . . . . 7 class ( (LFnl ` v ) X. (LFnl ` v ) )
18	16, 17	cres 4991	. . . . . 6 class ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) )
19	12, 18	cop 4020	. . . . 5 class <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >.
20	4, 13	cfv 5578	. . . . . 6 class (Scalar ` ndx )
21		coppr 17145	. . . . . . 7 class oppr
22	14, 21	cfv 5578	. . . . . 6 class (oppr ` (Scalar ` v ) )
23	20, 22	cop 4020	. . . . 5 class <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >.
24	10, 19, 23	ctp 4018	. . . 4 class { <. ( Base ` ndx ) , (LFnl ` v ) >. , <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >. , <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >. }
25		cvsca 14578	. . . . . . 7 class .s
26	4, 25	cfv 5578	. . . . . 6 class ( .s ` ndx )
27		vk	. . . . . . 7 setvar k
28		vf	. . . . . . 7 setvar f
29	14, 5	cfv 5578	. . . . . . 7 class ( Base ` (Scalar ` v ) )
30	28	cv 1382	. . . . . . . 8 class f
31	7, 5	cfv 5578	. . . . . . . . 9 class ( Base ` v )
32	27	cv 1382	. . . . . . . . . 10 class k
33	32	csn 4014	. . . . . . . . 9 class { k }
34	31, 33	cxp 4987	. . . . . . . 8 class ( ( Base ` v ) X. { k } )
35		cmulr 14575	. . . . . . . . . 10 class .r
36	14, 35	cfv 5578	. . . . . . . . 9 class ( .r ` (Scalar ` v ) )
37	36	cof 6523	. . . . . . . 8 class oF ( .r ` (Scalar ` v ) )
38	30, 34, 37	co 6281	. . . . . . 7 class ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) )
39	27, 28, 29, 9, 38	cmpt2 6283	. . . . . 6 class ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) )
40	26, 39	cop 4020	. . . . 5 class <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >.
41	40	csn 4014	. . . 4 class { <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >. }
42	24, 41	cun 3459	. . 3 class ( { <. ( Base ` ndx ) , (LFnl ` v ) >. , <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >. , <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >. } )
43	2, 3, 42	cmpt 4495	. 2 class ( v e. _V |-> ( { <. ( Base ` ndx ) , (LFnl ` v ) >. , <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >. , <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >. } ) )
44	1, 43	wceq 1383	1 wff LDual = ( v e. _V |-> ( { <. ( Base ` ndx ) , (LFnl ` v ) >. , <. ( +g ` ndx ) , ( oF ( +g ` (Scalar ` v ) ) |` ( (LFnl ` v ) X. (LFnl ` v ) ) ) >. , <. (Scalar ` ndx ) , (oppr ` (Scalar ` v ) ) >. } u. { <. ( .s ` ndx ) , ( k e. ( Base ` (Scalar ` v ) ) , f e. (LFnl ` v ) |-> ( f oF ( .r ` (Scalar ` v ) ) ( ( Base ` v ) X. { k } ) ) ) >. } ) )

This definition is referenced by:  ldualset  34590