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