Theorem lflcl

Description: A linear functional value is a scalar. (Contributed by NM, 15-Apr-2014)

	Ref	Expression
Hypotheses	lflf.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lflf.k	$$⊢K={\mathrm{Base}}_D$$
	lflf.v	$$⊢V={\mathrm{Base}}_W$$
	lflf.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
Assertion	lflcl	$$⊢\left(W\in Y\wedge G\in F\wedge X\in V\right)\to G\left(X\right)\in K$$

Proof

Step	Hyp	Ref	Expression
1		lflf.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
2		lflf.k	$$⊢K={\mathrm{Base}}_D$$
3		lflf.v	$$⊢V={\mathrm{Base}}_W$$
4		lflf.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
5	1 2 3 4	lflf	$$⊢\left(W\in Y\wedge G\in F\right)\to G:V⟶K$$
6	5	3adant3	$$⊢\left(W\in Y\wedge G\in F\wedge X\in V\right)\to G:V⟶K$$
7		simp3	$$⊢\left(W\in Y\wedge G\in F\wedge X\in V\right)\to X\in V$$
8	6 7	ffvelcdmd	$$⊢\left(W\in Y\wedge G\in F\wedge X\in V\right)\to G\left(X\right)\in K$$