Theorem ldualvsass2

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

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

Proof

Step	Hyp	Ref	Expression
1		ldualvsass2.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
2		ldualvsass2.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		ldualvsass2.k	$$⊢K={\mathrm{Base}}_R$$
4		ldualvsass2.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
5		ldualvsass2.q	$$⊢Q=\mathrm{Scalar}\left(D\right)$$
6		ldualvsass2.t	$$⊢\underset{\dot{}}{\times }={\cdot }_Q$$
7		ldualvsass2.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
8		ldualvsass2.w	$$⊢\phi \to W\in \mathrm{LMod}$$
9		ldualvsass2.x	$$⊢\phi \to X\in K$$
10		ldualvsass2.y	$$⊢\phi \to Y\in K$$
11		ldualvsass2.g	$$⊢\phi \to G\in F$$
12		eqid	$$⊢{\cdot }_R={\cdot }_R$$
13	2 3 12 4 5 6 8 9 10	ldualsmul	$$⊢\phi \to X\underset{\dot{}}{\times }Y=Y{\cdot }_{R}X$$
14	13	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{\times }Y\right)\underset{\dot{}}{·}G=\left(Y{\cdot }_{R}X\right)\underset{\dot{}}{·}G$$
15	1 2 3 12 4 7 8 9 10 11	ldualvsass	$$⊢\phi \to \left(Y{\cdot }_{R}X\right)\underset{\dot{}}{·}G=X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}G\right)$$
16	14 15	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{\times }Y\right)\underset{\dot{}}{·}G=X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}G\right)$$