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=BaseC
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=BaseC
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