Definition df-lfl 34345

Description: Define the set of all linear functionals (maps from vectors to the ring) of a left module or left vector space. (Contributed by NM, 15-Apr-2014.)

Assertion

Ref	Expression
df-lfl	|- LFnl = ( w e. _V |-> { f e. ( ( Base ` (Scalar ` w ) ) ^m ( Base ` w ) ) | A. r e. ( Base ` (Scalar ` w ) ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) ) } )

Distinct variable group:   x, w, y, r, f

Detailed syntax breakdown of Definition df-lfl

Step	Hyp	Ref	Expression
1		clfn 34344	. 2 class LFnl
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vr	. . . . . . . . . . . 12 setvar r
5	4	cv 1482	. . . . . . . . . . 11 class r
6		vx	. . . . . . . . . . . 12 setvar x
7	6	cv 1482	. . . . . . . . . . 11 class x
8	2	cv 1482	. . . . . . . . . . . 12 class w
9		cvsca 15945	. . . . . . . . . . . 12 class .s
10	8, 9	cfv 5888	. . . . . . . . . . 11 class ( .s ` w )
11	5, 7, 10	co 6650	. . . . . . . . . 10 class ( r ( .s ` w ) x )
12		vy	. . . . . . . . . . 11 setvar y
13	12	cv 1482	. . . . . . . . . 10 class y
14		cplusg 15941	. . . . . . . . . . 11 class +g
15	8, 14	cfv 5888	. . . . . . . . . 10 class ( +g ` w )
16	11, 13, 15	co 6650	. . . . . . . . 9 class ( ( r ( .s ` w ) x ) ( +g ` w ) y )
17		vf	. . . . . . . . . 10 setvar f
18	17	cv 1482	. . . . . . . . 9 class f
19	16, 18	cfv 5888	. . . . . . . 8 class ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) )
20	7, 18	cfv 5888	. . . . . . . . . 10 class ( f ` x )
21		csca 15944	. . . . . . . . . . . 12 class Scalar
22	8, 21	cfv 5888	. . . . . . . . . . 11 class (Scalar ` w )
23		cmulr 15942	. . . . . . . . . . 11 class .r
24	22, 23	cfv 5888	. . . . . . . . . 10 class ( .r ` (Scalar ` w ) )
25	5, 20, 24	co 6650	. . . . . . . . 9 class ( r ( .r ` (Scalar ` w ) ) ( f ` x ) )
26	13, 18	cfv 5888	. . . . . . . . 9 class ( f ` y )
27	22, 14	cfv 5888	. . . . . . . . 9 class ( +g ` (Scalar ` w ) )
28	25, 26, 27	co 6650	. . . . . . . 8 class ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) )
29	19, 28	wceq 1483	. . . . . . 7 wff ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) )
30		cbs 15857	. . . . . . . 8 class Base
31	8, 30	cfv 5888	. . . . . . 7 class ( Base ` w )
32	29, 12, 31	wral 2912	. . . . . 6 wff A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) )
33	32, 6, 31	wral 2912	. . . . 5 wff A. x e. ( Base ` w ) A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) )
34	22, 30	cfv 5888	. . . . 5 class ( Base ` (Scalar ` w ) )
35	33, 4, 34	wral 2912	. . . 4 wff A. r e. ( Base ` (Scalar ` w ) ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) )
36		cmap 7857	. . . . 5 class ^m
37	34, 31, 36	co 6650	. . . 4 class ( ( Base ` (Scalar ` w ) ) ^m ( Base ` w ) )
38	35, 17, 37	crab 2916	. . 3 class { f e. ( ( Base ` (Scalar ` w ) ) ^m ( Base ` w ) ) | A. r e. ( Base ` (Scalar ` w ) ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) ) }
39	2, 3, 38	cmpt 4729	. 2 class ( w e. _V |-> { f e. ( ( Base ` (Scalar ` w ) ) ^m ( Base ` w ) ) | A. r e. ( Base ` (Scalar ` w ) ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) ) } )
40	1, 39	wceq 1483	1 wff LFnl = ( w e. _V |-> { f e. ( ( Base ` (Scalar ` w ) ) ^m ( Base ` w ) ) | A. r e. ( Base ` (Scalar ` w ) ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` (Scalar ` w ) ) ( f ` x ) ) ( +g ` (Scalar ` w ) ) ( f ` y ) ) } )

This definition is referenced by:  lflset  34346