Description: Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | lcdval.h | |
|
Assertion | lcdfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcdval.h | |
|
2 | elex | |
|
3 | fveq2 | |
|
4 | 3 1 | eqtr4di | |
5 | fveq2 | |
|
6 | 5 | fveq1d | |
7 | 6 | fveq2d | |
8 | 6 | fveq2d | |
9 | fveq2 | |
|
10 | 9 | fveq1d | |
11 | 6 | fveq2d | |
12 | 11 | fveq1d | |
13 | 10 12 | fveq12d | |
14 | 10 13 | fveq12d | |
15 | 14 12 | eqeq12d | |
16 | 8 15 | rabeqbidv | |
17 | 7 16 | oveq12d | |
18 | 4 17 | mpteq12dv | |
19 | df-lcdual | |
|
20 | 18 19 1 | mptfvmpt | |
21 | 2 20 | syl | |