Metamath Proof Explorer


Theorem lcdlss

Description: Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses lcdlss.h H = LHyp K
lcdlss.o O = ocH K W
lcdlss.c C = LCDual K W
lcdlss.s S = LSubSp C
lcdlss.u U = DVecH K W
lcdlss.f F = LFnl U
lcdlss.l L = LKer U
lcdlss.d D = LDual U
lcdlss.t T = LSubSp D
lcdlss.b B = f F | O O L f = L f
lcdlss.k φ K HL W H
Assertion lcdlss φ S = T 𝒫 B

Proof

Step Hyp Ref Expression
1 lcdlss.h H = LHyp K
2 lcdlss.o O = ocH K W
3 lcdlss.c C = LCDual K W
4 lcdlss.s S = LSubSp C
5 lcdlss.u U = DVecH K W
6 lcdlss.f F = LFnl U
7 lcdlss.l L = LKer U
8 lcdlss.d D = LDual U
9 lcdlss.t T = LSubSp D
10 lcdlss.b B = f F | O O L f = L f
11 lcdlss.k φ K HL W H
12 1 2 3 5 6 7 8 11 10 lcdval2 φ C = D 𝑠 B
13 12 fveq2d φ LSubSp C = LSubSp D 𝑠 B
14 4 13 syl5eq φ S = LSubSp D 𝑠 B
15 14 eleq2d φ u S u LSubSp D 𝑠 B
16 1 5 11 dvhlmod φ U LMod
17 8 16 lduallmod φ D LMod
18 1 5 2 6 7 8 9 10 11 lclkr φ B T
19 eqid D 𝑠 B = D 𝑠 B
20 eqid LSubSp D 𝑠 B = LSubSp D 𝑠 B
21 19 9 20 lsslss D LMod B T u LSubSp D 𝑠 B u T u B
22 17 18 21 syl2anc φ u LSubSp D 𝑠 B u T u B
23 15 22 bitrd φ u S u T u B
24 elin u T 𝒫 B u T u 𝒫 B
25 velpw u 𝒫 B u B
26 25 anbi2i u T u 𝒫 B u T u B
27 24 26 bitr2i u T u B u T 𝒫 B
28 23 27 bitrdi φ u S u T 𝒫 B
29 28 eqrdv φ S = T 𝒫 B