Theorem lflcl

Description: A linear functional value is a scalar. (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	lflcl	|- ( ( W e. Y /\ G e. F /\ X e. V ) -> ( G ` X ) e. 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	1 2 3 4	lflf	|- ( ( W e. Y /\ G e. F ) -> G : V --> K )
6	5	3adant3	|- ( ( W e. Y /\ G e. F /\ X e. V ) -> G : V --> K )
7		simp3	|- ( ( W e. Y /\ G e. F /\ X e. V ) -> X e. V )
8	6 7	ffvelrnd	|- ( ( W e. Y /\ G e. F /\ X e. V ) -> ( G ` X ) e. K )