Metamath Proof Explorer


Theorem lcdfval

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

Ref Expression
Hypothesis lcdval.h H=LHypK
Assertion lcdfval KXLCDualK=wHLDualDVecHKw𝑠fLFnlDVecHKw|ocHKwocHKwLKerDVecHKwf=LKerDVecHKwf

Proof

Step Hyp Ref Expression
1 lcdval.h H=LHypK
2 elex KXKV
3 fveq2 k=KLHypk=LHypK
4 3 1 eqtr4di k=KLHypk=H
5 fveq2 k=KDVecHk=DVecHK
6 5 fveq1d k=KDVecHkw=DVecHKw
7 6 fveq2d k=KLDualDVecHkw=LDualDVecHKw
8 6 fveq2d k=KLFnlDVecHkw=LFnlDVecHKw
9 fveq2 k=KocHk=ocHK
10 9 fveq1d k=KocHkw=ocHKw
11 6 fveq2d k=KLKerDVecHkw=LKerDVecHKw
12 11 fveq1d k=KLKerDVecHkwf=LKerDVecHKwf
13 10 12 fveq12d k=KocHkwLKerDVecHkwf=ocHKwLKerDVecHKwf
14 10 13 fveq12d k=KocHkwocHkwLKerDVecHkwf=ocHKwocHKwLKerDVecHKwf
15 14 12 eqeq12d k=KocHkwocHkwLKerDVecHkwf=LKerDVecHkwfocHKwocHKwLKerDVecHKwf=LKerDVecHKwf
16 8 15 rabeqbidv k=KfLFnlDVecHkw|ocHkwocHkwLKerDVecHkwf=LKerDVecHkwf=fLFnlDVecHKw|ocHKwocHKwLKerDVecHKwf=LKerDVecHKwf
17 7 16 oveq12d k=KLDualDVecHkw𝑠fLFnlDVecHkw|ocHkwocHkwLKerDVecHkwf=LKerDVecHkwf=LDualDVecHKw𝑠fLFnlDVecHKw|ocHKwocHKwLKerDVecHKwf=LKerDVecHKwf
18 4 17 mpteq12dv k=KwLHypkLDualDVecHkw𝑠fLFnlDVecHkw|ocHkwocHkwLKerDVecHkwf=LKerDVecHkwf=wHLDualDVecHKw𝑠fLFnlDVecHKw|ocHKwocHKwLKerDVecHKwf=LKerDVecHKwf
19 df-lcdual LCDual=kVwLHypkLDualDVecHkw𝑠fLFnlDVecHkw|ocHkwocHkwLKerDVecHkwf=LKerDVecHkwf
20 18 19 1 mptfvmpt KVLCDualK=wHLDualDVecHKw𝑠fLFnlDVecHKw|ocHKwocHKwLKerDVecHKwf=LKerDVecHKwf
21 2 20 syl KXLCDualK=wHLDualDVecHKw𝑠fLFnlDVecHKw|ocHKwocHKwLKerDVecHKwf=LKerDVecHKwf