Theorem lflvsdi2

Description: Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014)

	Ref	Expression
Hypotheses	lfldi.v	$$⊢V={\mathrm{Base}}_W$$
	lfldi.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	lfldi.k	$$⊢K={\mathrm{Base}}_R$$
	lfldi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	lfldi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	lfldi.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lfldi.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lfldi.x	$$⊢\phi \to X\in K$$
	lfldi2.y	$$⊢\phi \to Y\in K$$
	lfldi2.g	$$⊢\phi \to G\in F$$
Assertion	lflvsdi2	$$⊢\phi \to G{\underset{\dot{}}{·}}_f\left(\left(V\times \left\{X\right\}\right){\underset{\dot{}}{+}}_f\left(V\times \left\{Y\right\}\right)\right)=\left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{Y\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lfldi.v	$$⊢V={\mathrm{Base}}_W$$
2		lfldi.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		lfldi.k	$$⊢K={\mathrm{Base}}_R$$
4		lfldi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
5		lfldi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6		lfldi.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
7		lfldi.w	$$⊢\phi \to W\in \mathrm{LMod}$$
8		lfldi.x	$$⊢\phi \to X\in K$$
9		lfldi2.y	$$⊢\phi \to Y\in K$$
10		lfldi2.g	$$⊢\phi \to G\in F$$
11	1	fvexi	$$⊢V\in \mathrm{V}$$
12	11	a1i	$$⊢\phi \to V\in \mathrm{V}$$
13	2 3 1 6	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to G:V⟶K$$
14	7 10 13	syl2anc	$$⊢\phi \to G:V⟶K$$
15		fconst6g	$$⊢X\in K\to \left(V\times \left\{X\right\}\right):V⟶K$$
16	8 15	syl	$$⊢\phi \to \left(V\times \left\{X\right\}\right):V⟶K$$
17		fconst6g	$$⊢Y\in K\to \left(V\times \left\{Y\right\}\right):V⟶K$$
18	9 17	syl	$$⊢\phi \to \left(V\times \left\{Y\right\}\right):V⟶K$$
19	2	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
20	7 19	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
21	3 4 5	ringdi	$$⊢\left(R\in \mathrm{Ring}\wedge \left(x\in K\wedge y\in K\wedge z\in K\right)\right)\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
22	20 21	sylan	$$⊢\left(\phi \wedge \left(x\in K\wedge y\in K\wedge z\in K\right)\right)\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
23	12 14 16 18 22	caofdi	$$⊢\phi \to G{\underset{\dot{}}{·}}_f\left(\left(V\times \left\{X\right\}\right){\underset{\dot{}}{+}}_f\left(V\times \left\{Y\right\}\right)\right)=\left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{Y\right\}\right)\right)$$