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=LHyp⁡K
lcdlmod.c ⊢C=LCDual⁡K⁡W
lcdlmod.k ⊢φ→K∈HL∧W∈H
Assertion lcdlvec ⊢φ→C∈LVec

Proof

Step Hyp Ref Expression
1 lcdlmod.h ⊢H=LHyp⁡K
2 lcdlmod.c ⊢C=LCDual⁡K⁡W
3 lcdlmod.k ⊢φ→K∈HL∧W∈H
4 eqid ⊢ocH⁡K⁡W=ocH⁡K⁡W
5 eqid ⊢DVecH⁡K⁡W=DVecH⁡K⁡W
6 eqid ⊢LFnl⁡DVecH⁡K⁡W=LFnl⁡DVecH⁡K⁡W
7 eqid ⊢LKer⁡DVecH⁡K⁡W=LKer⁡DVecH⁡K⁡W
8 eqid ⊢LDual⁡DVecH⁡K⁡W=LDual⁡DVecH⁡K⁡W
9 1 4 2 5 6 7 8 3 lcdval ⊢φ→C=LDual⁡DVecH⁡K⁡W↾𝑠f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f
10 1 5 3 dvhlvec ⊢φ→DVecH⁡K⁡W∈LVec
11 8 10 lduallvec ⊢φ→LDual⁡DVecH⁡K⁡W∈LVec
12 eqid ⊢LSubSp⁡LDual⁡DVecH⁡K⁡W=LSubSp⁡LDual⁡DVecH⁡K⁡W
13 eqid ⊢f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f=f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f
14 1 5 4 6 7 8 12 13 3 lclkr ⊢φ→f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f∈LSubSp⁡LDual⁡DVecH⁡K⁡W
15 eqid ⊢LDual⁡DVecH⁡K⁡W↾𝑠f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f=LDual⁡DVecH⁡K⁡W↾𝑠f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f
16 15 12 lsslvec ⊢LDual⁡DVecH⁡K⁡W∈LVec∧f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f∈LSubSp⁡LDual⁡DVecH⁡K⁡W→LDual⁡DVecH⁡K⁡W↾𝑠f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f∈LVec
17 11 14 16 syl2anc ⊢φ→LDual⁡DVecH⁡K⁡W↾𝑠f∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡f=LKer⁡DVecH⁡K⁡W⁡f∈LVec
18 9 17 eqeltrd ⊢φ→C∈LVec