Theorem ldualvsdi2

Description: Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	ldualvsdi2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	ldualvsdi2.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualvsdi2.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	ldualvsdi2.k	$$⊢K={\mathrm{Base}}_R$$
	ldualvsdi2.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualvsdi2.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
	ldualvsdi2.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	ldualvsdi2.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualvsdi2.x	$$⊢\phi \to X\in K$$
	ldualvsdi2.y	$$⊢\phi \to Y\in K$$
	ldualvsdi2.g	$$⊢\phi \to G\in F$$
Assertion	ldualvsdi2	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}G=\left(X\underset{\dot{}}{·}G\right)\underset{\dot{}}{✚}\left(Y\underset{\dot{}}{·}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		ldualvsdi2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvsdi2.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualvsdi2.a	$$⊢\underset{\dot{}}{+}={+}_R$$
4		ldualvsdi2.k	$$⊢K={\mathrm{Base}}_R$$
5		ldualvsdi2.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
6		ldualvsdi2.p	$$⊢\underset{\dot{}}{✚}={+}_D$$
7		ldualvsdi2.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
8		ldualvsdi2.w	$$⊢\phi \to W\in \mathrm{LMod}$$
9		ldualvsdi2.x	$$⊢\phi \to X\in K$$
10		ldualvsdi2.y	$$⊢\phi \to Y\in K$$
11		ldualvsdi2.g	$$⊢\phi \to G\in F$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13		eqid	$$⊢{\cdot }_R={\cdot }_R$$
14	2 4 3	lmodacl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in K\wedge Y\in K\right)\to X\underset{\dot{}}{+}Y\in K$$
15	8 9 10 14	syl3anc	$$⊢\phi \to X\underset{\dot{}}{+}Y\in K$$
16	1 12 2 4 13 5 7 8 15 11	ldualvs	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}G=G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\underset{\dot{}}{+}Y\right\}\right)$$
17	12 2 4 3 13 1 8 9 10 11	lflvsdi2a	$$⊢\phi \to G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\underset{\dot{}}{+}Y\right\}\right)=\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{Y\right\}\right)\right)$$
18	1 2 4 5 7 8 9 11	ldualvscl	$$⊢\phi \to X\underset{\dot{}}{·}G\in F$$
19	1 2 4 5 7 8 10 11	ldualvscl	$$⊢\phi \to Y\underset{\dot{}}{·}G\in F$$
20	1 2 3 5 6 8 18 19	ldualvadd	$$⊢\phi \to \left(X\underset{\dot{}}{·}G\right)\underset{\dot{}}{✚}\left(Y\underset{\dot{}}{·}G\right)=\left(X\underset{\dot{}}{·}G\right){\underset{\dot{}}{+}}_f\left(Y\underset{\dot{}}{·}G\right)$$
21	1 12 2 4 13 5 7 8 9 11	ldualvs	$$⊢\phi \to X\underset{\dot{}}{·}G=G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)$$
22	1 12 2 4 13 5 7 8 10 11	ldualvs	$$⊢\phi \to Y\underset{\dot{}}{·}G=G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{Y\right\}\right)$$
23	21 22	oveq12d	$$⊢\phi \to \left(X\underset{\dot{}}{·}G\right){\underset{\dot{}}{+}}_f\left(Y\underset{\dot{}}{·}G\right)=\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{Y\right\}\right)\right)$$
24	20 23	eqtr2d	$$⊢\phi \to \left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{Y\right\}\right)\right)=\left(X\underset{\dot{}}{·}G\right)\underset{\dot{}}{✚}\left(Y\underset{\dot{}}{·}G\right)$$
25	16 17 24	3eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}G=\left(X\underset{\dot{}}{·}G\right)\underset{\dot{}}{✚}\left(Y\underset{\dot{}}{·}G\right)$$