# Metamath Proof Explorer

## 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 ffvelrnd ${⊢}\left({W}\in {Y}\wedge {G}\in {F}\wedge {X}\in {V}\right)\to {G}\left({X}\right)\in {K}$