Theorem lfli

Description: Property of a linear functional. ( lnfnli analog.) (Contributed by NM, 16-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	lfli	$$⊢\left(W\in Z\wedge G\in F\wedge \left(R\in K\wedge X\in V\wedge Y\in V\right)\right)\to 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)$$

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	islfl	$$⊢W\in Z\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)$$
10	9	simplbda	$$⊢\left(W\in Z\wedge G\in F\right)\to \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)$$
11	10	3adant3	$$⊢\left(W\in Z\wedge G\in F\wedge \left(R\in K\wedge X\in V\wedge Y\in V\right)\right)\to \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)$$
12		oveq1	$$⊢r=R\to r\underset{\dot{}}{·}x=R\underset{\dot{}}{·}x$$
13	12	fvoveq1d	$$⊢r=R\to G\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=G\left(\left(R\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)$$
14		oveq1	$$⊢r=R\to r\underset{\dot{}}{\times }G\left(x\right)=R\underset{\dot{}}{\times }G\left(x\right)$$
15	14	oveq1d	$$⊢r=R\to \left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)=\left(R\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)$$
16	13 15	eqeq12d	$$⊢r=R\to \left(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)\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		oveq2	$$⊢x=X\to R\underset{\dot{}}{·}x=R\underset{\dot{}}{·}X$$
18	17	fvoveq1d	$$⊢x=X\to G\left(\left(R\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=G\left(\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}y\right)$$
19		fveq2	$$⊢x=X\to G\left(x\right)=G\left(X\right)$$
20	19	oveq2d	$$⊢x=X\to R\underset{\dot{}}{\times }G\left(x\right)=R\underset{\dot{}}{\times }G\left(X\right)$$
21	20	oveq1d	$$⊢x=X\to \left(R\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)=\left(R\underset{\dot{}}{\times }G\left(X\right)\right)\underset{\dot{}}{⨣}G\left(y\right)$$
22	18 21	eqeq12d	$$⊢x=X\to \left(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)\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)$$
23		oveq2	$$⊢y=Y\to \left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}y=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y$$
24	23	fveq2d	$$⊢y=Y\to G\left(\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}y\right)=G\left(\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y\right)$$
25		fveq2	$$⊢y=Y\to G\left(y\right)=G\left(Y\right)$$
26	25	oveq2d	$$⊢y=Y\to \left(R\underset{\dot{}}{\times }G\left(X\right)\right)\underset{\dot{}}{⨣}G\left(y\right)=\left(R\underset{\dot{}}{\times }G\left(X\right)\right)\underset{\dot{}}{⨣}G\left(Y\right)$$
27	24 26	eqeq12d	$$⊢y=Y\to \left(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)\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)$$
28	16 22 27	rspc3v	$$⊢\left(R\in K\wedge X\in V\wedge Y\in V\right)\to \left(\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)\to 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)$$
29	28	3ad2ant3	$$⊢\left(W\in Z\wedge G\in F\wedge \left(R\in K\wedge X\in V\wedge Y\in V\right)\right)\to \left(\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)\to 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)$$
30	11 29	mpd	$$⊢\left(W\in Z\wedge G\in F\wedge \left(R\in K\wedge X\in V\wedge Y\in V\right)\right)\to 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)$$