Metamath Proof Explorer

Theorem lcdlss2N

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

Ref Expression
Hypotheses lcdlss2.h ⊢ H = LHyp ⁡ K
lcdlss2.c ⊢ C = LCDual ⁡ K ⁡ W
lcdlss2.s ⊢ S = LSubSp ⁡ C
lcdlss2.v ⊢ V = Base C
lcdlss2.u ⊢ U = DVecH ⁡ K ⁡ W
lcdlss2.d ⊢ D = LDual ⁡ U
lcdlss2.t ⊢ T = LSubSp ⁡ D
lcdlss2.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion lcdlss2N ⊢ φ → S = T ∩ 𝒫 V

Proof

Step Hyp Ref Expression
1 lcdlss2.h ⊢ H = LHyp ⁡ K
2 lcdlss2.c ⊢ C = LCDual ⁡ K ⁡ W
3 lcdlss2.s ⊢ S = LSubSp ⁡ C
4 lcdlss2.v ⊢ V = Base C
5 lcdlss2.u ⊢ U = DVecH ⁡ K ⁡ W
6 lcdlss2.d ⊢ D = LDual ⁡ U
7 lcdlss2.t ⊢ T = LSubSp ⁡ D
8 lcdlss2.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
10 eqid ⊢ LFnl ⁡ U = LFnl ⁡ U
11 eqid ⊢ LKer ⁡ U = LKer ⁡ U
12 eqid ⊢ f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f = f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
13 1 9 2 3 5 10 11 6 7 12 8 lcdlss ⊢ φ → S = T ∩ 𝒫 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
14 1 9 2 4 5 10 11 12 8 lcdvbase ⊢ φ → V = f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
15 14 pweqd ⊢ φ → 𝒫 V = 𝒫 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
16 15 ineq2d ⊢ φ → T ∩ 𝒫 V = T ∩ 𝒫 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
17 13 16 eqtr4d ⊢ φ → S = T ∩ 𝒫 V