Description: Define the set of all linear functionals (maps from vectors to the ring) of a left module or left vector space. (Contributed by NM, 15-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-lfl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | clfn | |
|
1 | vw | |
|
2 | cvv | |
|
3 | vf | |
|
4 | cbs | |
|
5 | csca | |
|
6 | 1 | cv | |
7 | 6 5 | cfv | |
8 | 7 4 | cfv | |
9 | cmap | |
|
10 | 6 4 | cfv | |
11 | 8 10 9 | co | |
12 | vr | |
|
13 | vx | |
|
14 | vy | |
|
15 | 3 | cv | |
16 | 12 | cv | |
17 | cvsca | |
|
18 | 6 17 | cfv | |
19 | 13 | cv | |
20 | 16 19 18 | co | |
21 | cplusg | |
|
22 | 6 21 | cfv | |
23 | 14 | cv | |
24 | 20 23 22 | co | |
25 | 24 15 | cfv | |
26 | cmulr | |
|
27 | 7 26 | cfv | |
28 | 19 15 | cfv | |
29 | 16 28 27 | co | |
30 | 7 21 | cfv | |
31 | 23 15 | cfv | |
32 | 29 31 30 | co | |
33 | 25 32 | wceq | |
34 | 33 14 10 | wral | |
35 | 34 13 10 | wral | |
36 | 35 12 8 | wral | |
37 | 36 3 11 | crab | |
38 | 1 2 37 | cmpt | |
39 | 0 38 | wceq | |