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 = w V f Base Scalar w Base w | r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y

Detailed syntax breakdown

Step Hyp Ref Expression
0 clfn class LFnl
1 vw setvar w
2 cvv class V
3 vf setvar f
4 cbs class Base
5 csca class Scalar
6 1 cv setvar w
7 6 5 cfv class Scalar w
8 7 4 cfv class Base Scalar w
9 cmap class 𝑚
10 6 4 cfv class Base w
11 8 10 9 co class Base Scalar w Base w
12 vr setvar r
13 vx setvar x
14 vy setvar y
15 3 cv setvar f
16 12 cv setvar r
17 cvsca class 𝑠
18 6 17 cfv class w
19 13 cv setvar x
20 16 19 18 co class r w x
21 cplusg class + 𝑔
22 6 21 cfv class + w
23 14 cv setvar y
24 20 23 22 co class r w x + w y
25 24 15 cfv class f r w x + w y
26 cmulr class 𝑟
27 7 26 cfv class Scalar w
28 19 15 cfv class f x
29 16 28 27 co class r Scalar w f x
30 7 21 cfv class + Scalar w
31 23 15 cfv class f y
32 29 31 30 co class r Scalar w f x + Scalar w f y
33 25 32 wceq wff f r w x + w y = r Scalar w f x + Scalar w f y
34 33 14 10 wral wff y Base w f r w x + w y = r Scalar w f x + Scalar w f y
35 34 13 10 wral wff x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y
36 35 12 8 wral wff r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y
37 36 3 11 crab class f Base Scalar w Base w | r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y
38 1 2 37 cmpt class w V f Base Scalar w Base w | r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y
39 0 38 wceq wff LFnl = w V f Base Scalar w Base w | r Base Scalar w x Base w y Base w f r w x + w y = r Scalar w f x + Scalar w f y