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 )