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 = LHyp K
Assertion lcdfval K X LCDual K = w H LDual DVecH K w 𝑠 f LFnl DVecH K w | ocH K w ocH K w LKer DVecH K w f = LKer DVecH K w f

Proof

Step Hyp Ref Expression
1 lcdval.h H = LHyp K
2 elex K X K V
3 fveq2 k = K LHyp k = LHyp K
4 3 1 eqtr4di k = K LHyp k = H
5 fveq2 k = K DVecH k = DVecH K
6 5 fveq1d k = K DVecH k w = DVecH K w
7 6 fveq2d k = K LDual DVecH k w = LDual DVecH K w
8 6 fveq2d k = K LFnl DVecH k w = LFnl DVecH K w
9 fveq2 k = K ocH k = ocH K
10 9 fveq1d k = K ocH k w = ocH K w
11 6 fveq2d k = K LKer DVecH k w = LKer DVecH K w
12 11 fveq1d k = K LKer DVecH k w f = LKer DVecH K w f
13 10 12 fveq12d k = K ocH k w LKer DVecH k w f = ocH K w LKer DVecH K w f
14 10 13 fveq12d k = K ocH k w ocH k w LKer DVecH k w f = ocH K w ocH K w LKer DVecH K w f
15 14 12 eqeq12d k = K ocH k w ocH k w LKer DVecH k w f = LKer DVecH k w f ocH K w ocH K w LKer DVecH K w f = LKer DVecH K w f
16 8 15 rabeqbidv k = K f LFnl DVecH k w | ocH k w ocH k w LKer DVecH k w f = LKer DVecH k w f = f LFnl DVecH K w | ocH K w ocH K w LKer DVecH K w f = LKer DVecH K w f
17 7 16 oveq12d k = K LDual DVecH k w 𝑠 f LFnl DVecH k w | ocH k w ocH k w LKer DVecH k w f = LKer DVecH k w f = LDual DVecH K w 𝑠 f LFnl DVecH K w | ocH K w ocH K w LKer DVecH K w f = LKer DVecH K w f
18 4 17 mpteq12dv k = K w LHyp k LDual DVecH k w 𝑠 f LFnl DVecH k w | ocH k w ocH k w LKer DVecH k w f = LKer DVecH k w f = w H LDual DVecH K w 𝑠 f LFnl DVecH K w | ocH K w ocH K w LKer DVecH K w f = LKer DVecH K w f
19 df-lcdual LCDual = k V w LHyp k LDual DVecH k w 𝑠 f LFnl DVecH k w | ocH k w ocH k w LKer DVecH k w f = LKer DVecH k w f
20 18 19 1 mptfvmpt K V LCDual K = w H LDual DVecH K w 𝑠 f LFnl DVecH K w | ocH K w ocH K w LKer DVecH K w f = LKer DVecH K w f
21 2 20 syl K X LCDual K = w H LDual DVecH K w 𝑠 f LFnl DVecH K w | ocH K w ocH K w LKer DVecH K w f = LKer DVecH K w f