This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )