Metamath Proof Explorer

Definition df-lfl

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)

Ref Expression
Assertion 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clfn 
 |-  LFnl
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vf 
 |-  f
4 cbs 
 |-  Base
5 csca 
 |-  Scalar
6 1 cv 
 |-  w
7 6 5 cfv 
 |-  ( Scalar ` w )
8 7 4 cfv 
 |-  ( Base ` ( Scalar ` w ) )
9 cmap 
 |-  ^m
10 6 4 cfv 
 |-  ( Base ` w )
11 8 10 9 co 
 |-  ( ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) )
12 vr 
 |-  r
13 vx 
 |-  x
14 vy 
 |-  y
15 3 cv 
 |-  f
16 12 cv 
 |-  r
17 cvsca 
 |-  .s
18 6 17 cfv 
 |-  ( .s ` w )
19 13 cv 
 |-  x
20 16 19 18 co 
 |-  ( r ( .s ` w ) x )
21 cplusg 
 |-  +g
22 6 21 cfv 
 |-  ( +g ` w )
23 14 cv 
 |-  y
24 20 23 22 co 
 |-  ( ( r ( .s ` w ) x ) ( +g ` w ) y )
25 24 15 cfv 
 |-  ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) )
26 cmulr 
 |-  .r
27 7 26 cfv 
 |-  ( .r ` ( Scalar ` w ) )
28 19 15 cfv 
 |-  ( f ` x )
29 16 28 27 co 
 |-  ( r ( .r ` ( Scalar ` w ) ) ( f ` x ) )
30 7 21 cfv 
 |-  ( +g ` ( Scalar ` w ) )
31 23 15 cfv 
 |-  ( f ` y )
32 29 31 30 co 
 |-  ( ( r ( .r ` ( Scalar ` w ) ) ( f ` x ) ) ( +g ` ( Scalar ` w ) ) ( f ` y ) )
33 25 32 wceq 
 |-  ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` ( Scalar ` w ) ) ( f ` x ) ) ( +g ` ( Scalar ` w ) ) ( f ` y ) )
34 33 14 10 wral 
 |-  A. y e. ( Base ` w ) ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` ( Scalar ` w ) ) ( f ` x ) ) ( +g ` ( Scalar ` w ) ) ( f ` y ) )
35 34 13 10 wral 
 |-  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 35 12 8 wral 
 |-  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 ) )
37 36 3 11 crab 
 |-  { 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 ) ) }
38 1 2 37 cmpt 
 |-  ( 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 ) ) } )
39 0 38 wceq 
 |-  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 ) ) } )