Metamath Proof Explorer


Definition df-lfl

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 LFnl=wVfBaseScalarwBasew|rBaseScalarwxBasewyBasewfrwx+wy=rScalarwfx+Scalarwfy

Detailed syntax breakdown

Step Hyp Ref Expression
0 clfn classLFnl
1 vw setvarw
2 cvv classV
3 vf setvarf
4 cbs classBase
5 csca classScalar
6 1 cv setvarw
7 6 5 cfv classScalarw
8 7 4 cfv classBaseScalarw
9 cmap class𝑚
10 6 4 cfv classBasew
11 8 10 9 co classBaseScalarwBasew
12 vr setvarr
13 vx setvarx
14 vy setvary
15 3 cv setvarf
16 12 cv setvarr
17 cvsca class𝑠
18 6 17 cfv classw
19 13 cv setvarx
20 16 19 18 co classrwx
21 cplusg class+𝑔
22 6 21 cfv class+w
23 14 cv setvary
24 20 23 22 co classrwx+wy
25 24 15 cfv classfrwx+wy
26 cmulr class𝑟
27 7 26 cfv classScalarw
28 19 15 cfv classfx
29 16 28 27 co classrScalarwfx
30 7 21 cfv class+Scalarw
31 23 15 cfv classfy
32 29 31 30 co classrScalarwfx+Scalarwfy
33 25 32 wceq wfffrwx+wy=rScalarwfx+Scalarwfy
34 33 14 10 wral wffyBasewfrwx+wy=rScalarwfx+Scalarwfy
35 34 13 10 wral wffxBasewyBasewfrwx+wy=rScalarwfx+Scalarwfy
36 35 12 8 wral wffrBaseScalarwxBasewyBasewfrwx+wy=rScalarwfx+Scalarwfy
37 36 3 11 crab classfBaseScalarwBasew|rBaseScalarwxBasewyBasewfrwx+wy=rScalarwfx+Scalarwfy
38 1 2 37 cmpt classwVfBaseScalarwBasew|rBaseScalarwxBasewyBasewfrwx+wy=rScalarwfx+Scalarwfy
39 0 38 wceq wffLFnl=wVfBaseScalarwBasew|rBaseScalarwxBasewyBasewfrwx+wy=rScalarwfx+Scalarwfy