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=\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	lflf	$$⊢\left(W\in X\wedge G\in F\right)\to G:V⟶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		eqid	$$⊢{+}_W={+}_W$$
6		eqid	$$⊢{\cdot }_W={\cdot }_W$$
7		eqid	$$⊢{+}_D={+}_D$$
8		eqid	$$⊢{\cdot }_D={\cdot }_D$$
9	3 5 1 6 2 7 8 4	islfl	$$⊢W\in X\to \left(G\in F\leftrightarrow \left(G:V⟶K\wedge \forall r\in K\forall x\in V\forall y\in VG\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{D}G\left(x\right)\right){+}_{D}G\left(y\right)\right)\right)$$
10	9	simprbda	$$⊢\left(W\in X\wedge G\in F\right)\to G:V⟶K$$