# Metamath Proof Explorer

## Theorem lcdlvec

Description: The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses lcdlmod.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lcdlmod.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
lcdlmod.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion lcdlvec ${⊢}{\phi }\to {C}\in \mathrm{LVec}$

### Proof

Step Hyp Ref Expression
1 lcdlmod.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lcdlmod.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
3 lcdlmod.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
4 eqid ${⊢}\mathrm{ocH}\left({K}\right)\left({W}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
5 eqid ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
6 eqid ${⊢}\mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)=\mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
7 eqid ${⊢}\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
8 eqid ${⊢}\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)=\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)$
9 1 4 2 5 6 7 8 3 lcdval ${⊢}{\phi }\to {C}=\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right){↾}_{𝑠}\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}$
10 1 5 3 dvhlvec ${⊢}{\phi }\to \mathrm{DVecH}\left({K}\right)\left({W}\right)\in \mathrm{LVec}$
11 8 10 lduallvec ${⊢}{\phi }\to \mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\in \mathrm{LVec}$
12 eqid ${⊢}\mathrm{LSubSp}\left(\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\right)=\mathrm{LSubSp}\left(\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\right)$
13 eqid ${⊢}\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}=\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}$
14 1 5 4 6 7 8 12 13 3 lclkr ${⊢}{\phi }\to \left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}\in \mathrm{LSubSp}\left(\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\right)$
15 eqid ${⊢}\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right){↾}_{𝑠}\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}=\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right){↾}_{𝑠}\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}$
16 15 12 lsslvec ${⊢}\left(\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\in \mathrm{LVec}\wedge \left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}\in \mathrm{LSubSp}\left(\mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\right)\right)\to \mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right){↾}_{𝑠}\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}\in \mathrm{LVec}$
17 11 14 16 syl2anc ${⊢}{\phi }\to \mathrm{LDual}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right){↾}_{𝑠}\left\{{f}\in \mathrm{LFnl}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right)\right)=\mathrm{LKer}\left(\mathrm{DVecH}\left({K}\right)\left({W}\right)\right)\left({f}\right)\right\}\in \mathrm{LVec}$
18 9 17 eqeltrd ${⊢}{\phi }\to {C}\in \mathrm{LVec}$