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	$$⊢\mathrm{LFnl}=\left(w\in \mathrm{V}⟼\left\{f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}}^{{\mathrm{Base}}_w}\right)|\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{w}f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clfn	$$class\mathrm{LFnl}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		cbs	$$class\mathrm{Base}$$
5		csca	$$class\mathrm{Scalar}$$
6	1	cv	$$setvarw$$
7	6 5	cfv	$$class\mathrm{Scalar}\left(w\right)$$
8	7 4	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}$$
9		cmap	$$class{\uparrow }_{𝑚}$$
10	6 4	cfv	$$class{\mathrm{Base}}_w$$
11	8 10 9	co	$$class\left({{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}}^{{\mathrm{Base}}_w}\right)$$
12		vr	$$setvarr$$
13		vx	$$setvarx$$
14		vy	$$setvary$$
15	3	cv	$$setvarf$$
16	12	cv	$$setvarr$$
17		cvsca	$$class{\cdot }_{𝑠}$$
18	6 17	cfv	$$class{\cdot }_w$$
19	13	cv	$$setvarx$$
20	16 19 18	co	$$class\left(r{\cdot }_{w}x\right)$$
21		cplusg	$$class{+}_{𝑔}$$
22	6 21	cfv	$$class{+}_w$$
23	14	cv	$$setvary$$
24	20 23 22	co	$$class\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)$$
25	24 15	cfv	$$classf\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)$$
26		cmulr	$$class{\cdot }_{𝑟}$$
27	7 26	cfv	$$class{\cdot }_{\mathrm{Scalar}\left(w\right)}$$
28	19 15	cfv	$$classf\left(x\right)$$
29	16 28 27	co	$$class\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right)$$
30	7 21	cfv	$$class{+}_{\mathrm{Scalar}\left(w\right)}$$
31	23 15	cfv	$$classf\left(y\right)$$
32	29 31 30	co	$$class\left(\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)\right)$$
33	25 32	wceq	$$wfff\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)$$
34	33 14 10	wral	$$wff\forall y\in {\mathrm{Base}}_{w}f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)$$
35	34 13 10	wral	$$wff\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{w}f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)$$
36	35 12 8	wral	$$wff\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{w}f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)$$
37	36 3 11	crab	$$class\left\{f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}}^{{\mathrm{Base}}_w}\right)|\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{w}f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)\right\}$$
38	1 2 37	cmpt	$$class\left(w\in \mathrm{V}⟼\left\{f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}}^{{\mathrm{Base}}_w}\right)|\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{w}f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)\right\}\right)$$
39	0 38	wceq	$$wff\mathrm{LFnl}=\left(w\in \mathrm{V}⟼\left\{f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}}^{{\mathrm{Base}}_w}\right)|\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{w}f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)\right\}\right)$$