Theorem lflvsass

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

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

Proof

Step	Hyp	Ref	Expression
1		lflass.v	$$⊢V={\mathrm{Base}}_W$$
2		lflass.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
3		lflass.k	$$⊢K={\mathrm{Base}}_R$$
4		lflass.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
5		lflass.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
6		lflass.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		lflass.x	$$⊢\phi \to X\in K$$
8		lflass.y	$$⊢\phi \to Y\in K$$
9		lflass.g	$$⊢\phi \to G\in F$$
10	1	fvexi	$$⊢V\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to V\in \mathrm{V}$$
12	2 3 1 5	lflf	$$⊢\left(W\in \mathrm{LMod}\wedge G\in F\right)\to G:V⟶K$$
13	6 9 12	syl2anc	$$⊢\phi \to G:V⟶K$$
14		fconst6g	$$⊢X\in K\to \left(V\times \left\{X\right\}\right):V⟶K$$
15	7 14	syl	$$⊢\phi \to \left(V\times \left\{X\right\}\right):V⟶K$$
16		fconst6g	$$⊢Y\in K\to \left(V\times \left\{Y\right\}\right):V⟶K$$
17	8 16	syl	$$⊢\phi \to \left(V\times \left\{Y\right\}\right):V⟶K$$
18	2	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
19	6 18	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
20	3 4	ringass	$$⊢\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=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
21	19 20	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=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
22	11 13 15 17 21	caofass	$$⊢\phi \to \left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)\right){\underset{\dot{}}{·}}_f\left(V\times \left\{Y\right\}\right)=G{\underset{\dot{}}{·}}_f\left(\left(V\times \left\{X\right\}\right){\underset{\dot{}}{·}}_f\left(V\times \left\{Y\right\}\right)\right)$$
23	11 7 8	ofc12	$$⊢\phi \to \left(V\times \left\{X\right\}\right){\underset{\dot{}}{·}}_f\left(V\times \left\{Y\right\}\right)=V\times \left\{X\underset{\dot{}}{·}Y\right\}$$
24	23	oveq2d	$$⊢\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)=G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\underset{\dot{}}{·}Y\right\}\right)$$
25	22 24	eqtr2d	$$⊢\phi \to G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\underset{\dot{}}{·}Y\right\}\right)=\left(G{\underset{\dot{}}{·}}_f\left(V\times \left\{X\right\}\right)\right){\underset{\dot{}}{·}}_f\left(V\times \left\{Y\right\}\right)$$