Theorem lflvsdi1

Description: 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$$
	lfldi1.g	$$⊢\phi \to G\in F$$
	lfldi1.h	$$⊢\phi \to H\in F$$
Assertion	lflvsdi1	$$⊢\phi \to \left(G{\underset{\dot{}}{+}}_{f}H\right){\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)=\left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)\right){\underset{\dot{}}{+}}_f\left(H{\underset{\dot{}}{·}}_f\left(V\times \left\{X\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		lfldi1.g	$$⊢\phi \to G\in F$$
10		lfldi1.h	$$⊢\phi \to H\in F$$
11	1	fvexi	$$⊢V\in \mathrm{V}$$
12	11	a1i	$$⊢\phi \to V\in \mathrm{V}$$
13		fconst6g	$$⊢X\in K\to \left(V\times \left\{X\right\}\right):V⟶K$$
14	8 13	syl	$$⊢\phi \to \left(V\times \left\{X\right\}\right):V⟶K$$
15	2 3 1 6	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to G:V⟶K$$
16	7 9 15	syl2anc	$$⊢\phi \to G:V⟶K$$
17	2 3 1 6	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge H\in F\right)\to H:V⟶K$$
18	7 10 17	syl2anc	$$⊢\phi \to H: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	ringdir	$$⊢\left(R\in \mathrm{Ring}\wedge \left(x\in K\wedge y\in K\wedge z\in K\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\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 \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
23	12 14 16 18 22	caofdir	$$⊢\phi \to \left(G{\underset{\dot{}}{+}}_{f}H\right){\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)=\left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)\right){\underset{\dot{}}{+}}_f\left(H{\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)\right)$$