# Metamath Proof Explorer

## Theorem lcdvbaselfl

Description: A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdvbasess.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lcdvbasess.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
lcdvbasess.v ${⊢}{V}={\mathrm{Base}}_{{C}}$
lcdvbasess.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lcdvbasess.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
lcdvbasess.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
lcdvbaselfl.x ${⊢}{\phi }\to {X}\in {V}$
Assertion lcdvbaselfl ${⊢}{\phi }\to {X}\in {F}$

### Proof

Step Hyp Ref Expression
1 lcdvbasess.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcdvbasess.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
3 lcdvbasess.v ${⊢}{V}={\mathrm{Base}}_{{C}}$
4 lcdvbasess.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 lcdvbasess.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
6 lcdvbasess.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 lcdvbaselfl.x ${⊢}{\phi }\to {X}\in {V}$
8 1 2 3 4 5 6 lcdvbasess ${⊢}{\phi }\to {V}\subseteq {F}$
9 8 7 sseldd ${⊢}{\phi }\to {X}\in {F}$