Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lfl Unicode version

Definition df-lfl 29870
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
StepHypRef Expression
1 clfn 29869 . 2  class LFnl
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
4 vr . . . . . . . . . . . 12  set  r
54cv 1631 . . . . . . . . . . 11  class  r
6 vx . . . . . . . . . . . 12  set  x
76cv 1631 . . . . . . . . . . 11  class  x
82cv 1631 . . . . . . . . . . . 12  class  w
9 cvsca 13228 . . . . . . . . . . . 12  class  .s
108, 9cfv 5271 . . . . . . . . . . 11  class  ( .s
`  w )
115, 7, 10co 5874 . . . . . . . . . 10  class  ( r ( .s `  w
) x )
12 vy . . . . . . . . . . 11  set  y
1312cv 1631 . . . . . . . . . 10  class  y
14 cplusg 13224 . . . . . . . . . . 11  class  +g
158, 14cfv 5271 . . . . . . . . . 10  class  ( +g  `  w )
1611, 13, 15co 5874 . . . . . . . . 9  class  ( ( r ( .s `  w ) x ) ( +g  `  w
) y )
17 vf . . . . . . . . . 10  set  f
1817cv 1631 . . . . . . . . 9  class  f
1916, 18cfv 5271 . . . . . . . 8  class  ( f `
 ( ( r ( .s `  w
) x ) ( +g  `  w ) y ) )
207, 18cfv 5271 . . . . . . . . . 10  class  ( f `
 x )
21 csca 13227 . . . . . . . . . . . 12  class Scalar
228, 21cfv 5271 . . . . . . . . . . 11  class  (Scalar `  w )
23 cmulr 13225 . . . . . . . . . . 11  class  .r
2422, 23cfv 5271 . . . . . . . . . 10  class  ( .r
`  (Scalar `  w )
)
255, 20, 24co 5874 . . . . . . . . 9  class  ( r ( .r `  (Scalar `  w ) ) ( f `  x ) )
2613, 18cfv 5271 . . . . . . . . 9  class  ( f `
 y )
2722, 14cfv 5271 . . . . . . . . 9  class  ( +g  `  (Scalar `  w )
)
2825, 26, 27co 5874 . . . . . . . 8  class  ( ( r ( .r `  (Scalar `  w ) ) ( f `  x
) ) ( +g  `  (Scalar `  w )
) ( f `  y ) )
2919, 28wceq 1632 . . . . . . 7  wff  ( f `
 ( ( r ( .s `  w
) x ) ( +g  `  w ) y ) )  =  ( ( r ( .r `  (Scalar `  w ) ) ( f `  x ) ) ( +g  `  (Scalar `  w ) ) ( f `  y ) )
30 cbs 13164 . . . . . . . 8  class  Base
318, 30cfv 5271 . . . . . . 7  class  ( Base `  w )
3229, 12, 31wral 2556 . . . . . 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 ) )
3332, 6, 31wral 2556 . . . . 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 ) )
3422, 30cfv 5271 . . . . 5  class  ( Base `  (Scalar `  w )
)
3533, 4, 34wral 2556 . . . 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 6788 . . . . 5  class  ^m
3734, 31, 36co 5874 . . . 4  class  ( (
Base `  (Scalar `  w
) )  ^m  ( Base `  w ) )
3835, 17, 37crab 2560 . . 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 ) ) }
392, 3, 38cmpt 4093 . 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 ) ) } )
401, 39wceq 1632 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 ) ) } )
Colors of variables: wff set class
This definition is referenced by:  lflset  29871
  Copyright terms: Public domain W3C validator