Metamath Proof Explorer

Theorem lflset

Description: The set of linear functionals in a left module or left vector space. (Contributed by NM, 15-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lflset.v 
|- V = ( Base ` W )
lflset.a 
|- .+ = ( +g ` W )
lflset.d 
|- D = ( Scalar ` W )
lflset.s 
|- .x. = ( .s ` W )
lflset.k 
|- K = ( Base ` D )
lflset.p 
|- .+^ = ( +g ` D )
lflset.t 
|- .X. = ( .r ` D )
lflset.f 
|- F = ( LFnl ` W )
Assertion lflset 
|- ( W e. X -> F = { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } )

Proof

Step Hyp Ref Expression
1 lflset.v 
 |-  V = ( Base ` W )
2 lflset.a 
 |-  .+ = ( +g ` W )
3 lflset.d 
 |-  D = ( Scalar ` W )
4 lflset.s 
 |-  .x. = ( .s ` W )
5 lflset.k 
 |-  K = ( Base ` D )
6 lflset.p 
 |-  .+^ = ( +g ` D )
7 lflset.t 
 |-  .X. = ( .r ` D )
8 lflset.f 
 |-  F = ( LFnl ` W )
9 elex 
 |-  ( W e. X -> W e. _V )
10 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
11 10 3 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = D )
12 11 fveq2d 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = ( Base ` D ) )
13 12 5 eqtr4di 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = K )
14 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
15 14 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
16 13 15 oveq12d 
 |-  ( w = W -> ( ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) ) = ( K ^m V ) )
17 fveq2 
 |-  ( w = W -> ( +g ` w ) = ( +g ` W ) )
18 17 2 eqtr4di 
 |-  ( w = W -> ( +g ` w ) = .+ )
19 fveq2 
 |-  ( w = W -> ( .s ` w ) = ( .s ` W ) )
20 19 4 eqtr4di 
 |-  ( w = W -> ( .s ` w ) = .x. )
21 20 oveqd 
 |-  ( w = W -> ( r ( .s ` w ) x ) = ( r .x. x ) )
22 eqidd 
 |-  ( w = W -> y = y )
23 18 21 22 oveq123d 
 |-  ( w = W -> ( ( r ( .s ` w ) x ) ( +g ` w ) y ) = ( ( r .x. x ) .+ y ) )
24 23 fveq2d 
 |-  ( w = W -> ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( f ` ( ( r .x. x ) .+ y ) ) )
25 11 fveq2d 
 |-  ( w = W -> ( +g ` ( Scalar ` w ) ) = ( +g ` D ) )
26 25 6 eqtr4di 
 |-  ( w = W -> ( +g ` ( Scalar ` w ) ) = .+^ )
27 11 fveq2d 
 |-  ( w = W -> ( .r ` ( Scalar ` w ) ) = ( .r ` D ) )
28 27 7 eqtr4di 
 |-  ( w = W -> ( .r ` ( Scalar ` w ) ) = .X. )
29 28 oveqd 
 |-  ( w = W -> ( r ( .r ` ( Scalar ` w ) ) ( f ` x ) ) = ( r .X. ( f ` x ) ) )
30 eqidd 
 |-  ( w = W -> ( f ` y ) = ( f ` y ) )
31 26 29 30 oveq123d 
 |-  ( w = W -> ( ( r ( .r ` ( Scalar ` w ) ) ( f ` x ) ) ( +g ` ( Scalar ` w ) ) ( f ` y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) )
32 24 31 eqeq12d 
 |-  ( w = W -> ( ( f ` ( ( r ( .s ` w ) x ) ( +g ` w ) y ) ) = ( ( r ( .r ` ( Scalar ` w ) ) ( f ` x ) ) ( +g ` ( Scalar ` w ) ) ( f ` y ) ) <-> ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) ) )
33 15 32 raleqbidv 
 |-  ( w = 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 ) ) <-> A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) ) )
34 15 33 raleqbidv 
 |-  ( w = 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 ) ) <-> A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) ) )
35 13 34 raleqbidv 
 |-  ( w = 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 ) ) <-> A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) ) )
36 16 35 rabeqbidv 
 |-  ( w = W -> { 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 ) ) } = { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } )
37 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 ) ) } )
38 ovex 
 |-  ( K ^m V ) e. _V
39 38 rabex 
 |-  { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } e. _V
40 36 37 39 fvmpt 
 |-  ( W e. _V -> ( LFnl ` W ) = { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } )
41 8 40 syl5eq 
 |-  ( W e. _V -> F = { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } )
42 9 41 syl 
 |-  ( W e. X -> F = { f e. ( K ^m V ) | A. r e. K A. x e. V A. y e. V ( f ` ( ( r .x. x ) .+ y ) ) = ( ( r .X. ( f ` x ) ) .+^ ( f ` y ) ) } )