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