Theorem islfl

Description: The predicate "is a linear functional". (Contributed by NM, 15-Apr-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	islfl	$$⊢W\in X\to \left(G\in F\leftrightarrow \left(G:V⟶K\wedge \forall r\in K\forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\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	1 2 3 4 5 6 7 8	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\}$$
10	9	eleq2d	$$⊢W\in X\to \left(G\in F\leftrightarrow G\in \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\}\right)$$
11		fveq1	$$⊢f=G\to f\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=G\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)$$
12		fveq1	$$⊢f=G\to f\left(x\right)=G\left(x\right)$$
13	12	oveq2d	$$⊢f=G\to r\underset{\dot{}}{\times }f\left(x\right)=r\underset{\dot{}}{\times }G\left(x\right)$$
14		fveq1	$$⊢f=G\to f\left(y\right)=G\left(y\right)$$
15	13 14	oveq12d	$$⊢f=G\to \left(r\underset{\dot{}}{\times }f\left(x\right)\right)\underset{\dot{}}{⨣}f\left(y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)$$
16	11 15	eqeq12d	$$⊢f=G\to \left(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)\leftrightarrow G\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)$$
17	16	2ralbidv	$$⊢f=G\to \left(\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)\leftrightarrow \forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)$$
18	17	ralbidv	$$⊢f=G\to \left(\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)\leftrightarrow \forall r\in K\forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)$$
19	18	elrab	$$⊢G\in \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\}\leftrightarrow \left(G\in \left(K^V\right)\wedge \forall r\in K\forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)$$
20	5	fvexi	$$⊢K\in \mathrm{V}$$
21	1	fvexi	$$⊢V\in \mathrm{V}$$
22	20 21	elmap	$$⊢G\in \left(K^V\right)\leftrightarrow G:V⟶K$$
23	22	anbi1i	$$⊢\left(G\in \left(K^V\right)\wedge \forall r\in K\forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)\leftrightarrow \left(G:V⟶K\wedge \forall r\in K\forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)$$
24	19 23	bitri	$$⊢G\in \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\}\leftrightarrow \left(G:V⟶K\wedge \forall r\in K\forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)$$
25	10 24	syl6bb	$$⊢W\in X\to \left(G\in F\leftrightarrow \left(G:V⟶K\wedge \forall r\in K\forall x\in V\forall y\in VG\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=\left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)\right)\right)$$