Theorem lflset

Description: The set of linear functionals in a left module or left vector space. (Contributed by NM, 15-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lflset.v	$$⊢V={\mathrm{Base}}_W$$
	lflset.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	lflset.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
	lflset.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lflset.k	$$⊢K={\mathrm{Base}}_D$$
	lflset.p	$$⊢\underset{\dot{}}{⨣}={+}_D$$
	lflset.t	$$⊢\underset{\dot{}}{\times }={\cdot }_D$$
	lflset.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
Assertion	lflset	$$⊢W\in X\to F=\left\{f\in \left(K^V\right)|\forall r\in K\forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lflset.v	$$⊢V={\mathrm{Base}}_W$$
2		lflset.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lflset.d	$$⊢D=\mathrm{Scalar}\left(W\right)$$
4		lflset.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		lflset.k	$$⊢K={\mathrm{Base}}_D$$
6		lflset.p	$$⊢\underset{\dot{}}{⨣}={+}_D$$
7		lflset.t	$$⊢\underset{\dot{}}{\times }={\cdot }_D$$
8		lflset.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
9		elex	$$⊢W\in X\to W\in \mathrm{V}$$
10		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
11	10 3	eqtr4di	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=D$$
12	11	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}={\mathrm{Base}}_D$$
13	12 5	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}=K$$
14		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
15	14 1	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=V$$
16	13 15	oveq12d	$$⊢w=W\to {{\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}}^{{\mathrm{Base}}_w}=K^V$$
17		fveq2	$$⊢w=W\to {+}_w={+}_W$$
18	17 2	eqtr4di	$$⊢w=W\to {+}_w=\underset{\dot{}}{+}$$
19		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
20	19 4	eqtr4di	$$⊢w=W\to {\cdot }_w=\underset{\dot{}}{·}$$
21	20	oveqd	$$⊢w=W\to r{\cdot }_{w}x=r\underset{\dot{}}{·}x$$
22		eqidd	$$⊢w=W\to y=y$$
23	18 21 22	oveq123d	$$⊢w=W\to \left(r{\cdot }_{w}x\right){+}_{w}y=\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y$$
24	23	fveq2d	$$⊢w=W\to f\left(\left(r{\cdot }_{w}x\right){+}_{w}y\right)=f\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)$$
25	11	fveq2d	$$⊢w=W\to {+}_{\mathrm{Scalar}\left(w\right)}={+}_D$$
26	25 6	eqtr4di	$$⊢w=W\to {+}_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{⨣}$$
27	11	fveq2d	$$⊢w=W\to {\cdot }_{\mathrm{Scalar}\left(w\right)}={\cdot }_D$$
28	27 7	eqtr4di	$$⊢w=W\to {\cdot }_{\mathrm{Scalar}\left(w\right)}=\underset{\dot{}}{\times }$$
29	28	oveqd	$$⊢w=W\to r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)=r\underset{\dot{}}{\times }f\left(x\right)$$
30		eqidd	$$⊢w=W\to f\left(y\right)=f\left(y\right)$$
31	26 29 30	oveq123d	$$⊢w=W\to \left(r{\cdot }_{\mathrm{Scalar}\left(w\right)}f\left(x\right)\right){+}_{\mathrm{Scalar}\left(w\right)}f\left(y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)$$
32	24 31	eqeq12d	$$⊢w=W\to \left(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)\leftrightarrow f\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right)$$
33	15 32	raleqbidv	$$⊢w=W\to \left(\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)\leftrightarrow \forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right)$$
34	15 33	raleqbidv	$$⊢w=W\to \left(\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)\leftrightarrow \forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right)$$
35	13 34	raleqbidv	$$⊢w=W\to \left(\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)\leftrightarrow \forall r\in K\forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right)$$
36	16 35	rabeqbidv	$$⊢w=W\to \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\}=\left\{f\in \left(K^V\right)|\forall r\in K\forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right\}$$
37		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)$$
38		ovex	$$⊢K^V\in \mathrm{V}$$
39	38	rabex	$$⊢\left\{f\in \left(K^V\right)|\forall r\in K\forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right\}\in \mathrm{V}$$
40	36 37 39	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{LFnl}\left(W\right)=\left\{f\in \left(K^V\right)|\forall r\in K\forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right\}$$
41	8 40	syl5eq	$$⊢W\in \mathrm{V}\to F=\left\{f\in \left(K^V\right)|\forall r\in K\forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right\}$$
42	9 41	syl	$$⊢W\in X\to F=\left\{f\in \left(K^V\right)|\forall r\in K\forall x\in V\forall y\in Vf\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)\right\}$$