Metamath Proof Explorer


Theorem lflf

Description: A linear functional is a function from vectors to scalars. ( lnfnfi analog.) (Contributed by NM, 15-Apr-2014)

Ref Expression
Hypotheses lflf.d
|- D = ( Scalar ` W )
lflf.k
|- K = ( Base ` D )
lflf.v
|- V = ( Base ` W )
lflf.f
|- F = ( LFnl ` W )
Assertion lflf
|- ( ( W e. X /\ G e. F ) -> G : V --> K )

Proof

Step Hyp Ref Expression
1 lflf.d
 |-  D = ( Scalar ` W )
2 lflf.k
 |-  K = ( Base ` D )
3 lflf.v
 |-  V = ( Base ` W )
4 lflf.f
 |-  F = ( LFnl ` W )
5 eqid
 |-  ( +g ` W ) = ( +g ` W )
6 eqid
 |-  ( .s ` W ) = ( .s ` W )
7 eqid
 |-  ( +g ` D ) = ( +g ` D )
8 eqid
 |-  ( .r ` D ) = ( .r ` D )
9 3 5 1 6 2 7 8 4 islfl
 |-  ( W e. X -> ( G e. F <-> ( G : V --> K /\ A. r e. K A. x e. V A. y e. V ( G ` ( ( r ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( r ( .r ` D ) ( G ` x ) ) ( +g ` D ) ( G ` y ) ) ) ) )
10 9 simprbda
 |-  ( ( W e. X /\ G e. F ) -> G : V --> K )