Description: Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | hdmap1val.h | |
|
Assertion | hdmap1ffval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hdmap1val.h | |
|
2 | elex | |
|
3 | fveq2 | |
|
4 | 3 1 | eqtr4di | |
5 | fveq2 | |
|
6 | 5 | fveq1d | |
7 | fveq2 | |
|
8 | 7 | fveq1d | |
9 | fveq2 | |
|
10 | 9 | fveq1d | |
11 | 10 | sbceq1d | |
12 | 11 | sbcbidv | |
13 | 12 | sbcbidv | |
14 | 8 13 | sbceqbid | |
15 | 14 | sbcbidv | |
16 | 15 | sbcbidv | |
17 | 6 16 | sbceqbid | |
18 | 17 | abbidv | |
19 | 4 18 | mpteq12dv | |
20 | df-hdmap1 | |
|
21 | 19 20 1 | mptfvmpt | |
22 | 2 21 | syl | |