Theorem ldualvsdi1

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

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

Proof

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