Theorem islfld

Description: Properties that determine a linear functional. TODO: use this in place of islfl when it shortens the proof. (Contributed by NM, 19-Oct-2014)

	Ref	Expression
Hypotheses	islfld.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
	islfld.a	$$⊢\phi \to \underset{\dot{}}{+}={+}_W$$
	islfld.d	$$⊢\phi \to D=\mathrm{Scalar}\left(W\right)$$
	islfld.s	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
	islfld.k	$$⊢\phi \to K={\mathrm{Base}}_D$$
	islfld.p	$$⊢\phi \to \underset{\dot{}}{⨣}={+}_D$$
	islfld.t	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_D$$
	islfld.f	$$⊢\phi \to F=\mathrm{LFnl}\left(W\right)$$
	islfld.u	$$⊢\phi \to G:V⟶K$$
	islfld.l	$$⊢\left(\phi \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)$$
	islfld.w	$$⊢\phi \to W\in X$$
Assertion	islfld	$$⊢\phi \to G\in F$$

Proof

Step	Hyp	Ref	Expression
1		islfld.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
2		islfld.a	$$⊢\phi \to \underset{\dot{}}{+}={+}_W$$
3		islfld.d	$$⊢\phi \to D=\mathrm{Scalar}\left(W\right)$$
4		islfld.s	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
5		islfld.k	$$⊢\phi \to K={\mathrm{Base}}_D$$
6		islfld.p	$$⊢\phi \to \underset{\dot{}}{⨣}={+}_D$$
7		islfld.t	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_D$$
8		islfld.f	$$⊢\phi \to F=\mathrm{LFnl}\left(W\right)$$
9		islfld.u	$$⊢\phi \to G:V⟶K$$
10		islfld.l	$$⊢\left(\phi \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)$$
11		islfld.w	$$⊢\phi \to W\in X$$
12	3	fveq2d	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
13	5 12	eqtrd	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
14	1 13	feq23d	$$⊢\phi \to \left(G:V⟶K\leftrightarrow G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)$$
15	9 14	mpbid	$$⊢\phi \to G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
16	10	ralrimivvva	$$⊢\phi \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)$$
17	4	oveqd	$$⊢\phi \to r\underset{\dot{}}{·}x=r{\cdot }_{W}x$$
18		eqidd	$$⊢\phi \to y=y$$
19	2 17 18	oveq123d	$$⊢\phi \to \left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y=\left(r{\cdot }_{W}x\right){+}_{W}y$$
20	19	fveq2d	$$⊢\phi \to G\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{+}y\right)=G\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)$$
21	3	fveq2d	$$⊢\phi \to {+}_D={+}_{\mathrm{Scalar}\left(W\right)}$$
22	6 21	eqtrd	$$⊢\phi \to \underset{\dot{}}{⨣}={+}_{\mathrm{Scalar}\left(W\right)}$$
23	3	fveq2d	$$⊢\phi \to {\cdot }_D={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
24	7 23	eqtrd	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
25	24	oveqd	$$⊢\phi \to r\underset{\dot{}}{\times }G\left(x\right)=r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)$$
26		eqidd	$$⊢\phi \to G\left(y\right)=G\left(y\right)$$
27	22 25 26	oveq123d	$$⊢\phi \to \left(r\underset{\dot{}}{\times }G\left(x\right)\right)\underset{\dot{}}{⨣}G\left(y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)$$
28	20 27	eqeq12d	$$⊢\phi \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{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)\right)$$
29	1 28	raleqbidv	$$⊢\phi \to \left(\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)\leftrightarrow \forall y\in {\mathrm{Base}}_{W}G\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)\right)$$
30	1 29	raleqbidv	$$⊢\phi \to \left(\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)\leftrightarrow \forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_{W}G\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)\right)$$
31	13 30	raleqbidv	$$⊢\phi \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)\leftrightarrow \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_{W}G\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)\right)$$
32	16 31	mpbid	$$⊢\phi \to \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_{W}G\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)$$
33		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
34		eqid	$$⊢{+}_W={+}_W$$
35		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
36		eqid	$$⊢{\cdot }_W={\cdot }_W$$
37		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
38		eqid	$$⊢{+}_{\mathrm{Scalar}\left(W\right)}={+}_{\mathrm{Scalar}\left(W\right)}$$
39		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(W\right)}={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
40		eqid	$$⊢\mathrm{LFnl}\left(W\right)=\mathrm{LFnl}\left(W\right)$$
41	33 34 35 36 37 38 39 40	islfl	$$⊢W\in X\to \left(G\in \mathrm{LFnl}\left(W\right)\leftrightarrow \left(G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_{W}G\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)\right)\right)$$
42	41	biimpar	$$⊢\left(W\in X\wedge \left(G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_{W}G\left(\left(r{\cdot }_{W}x\right){+}_{W}y\right)=\left(r{\cdot }_{\mathrm{Scalar}\left(W\right)}G\left(x\right)\right){+}_{\mathrm{Scalar}\left(W\right)}G\left(y\right)\right)\right)\to G\in \mathrm{LFnl}\left(W\right)$$
43	11 15 32 42	syl12anc	$$⊢\phi \to G\in \mathrm{LFnl}\left(W\right)$$
44	43 8	eleqtrrd	$$⊢\phi \to G\in F$$