Theorem clmvsdi

Description: Distributive law for scalar product (left-distributivity). ( lmodvsdi analog.) (Contributed by NM, 3-Nov-2006) (Revised by AV, 28-Sep-2021)

	Ref	Expression
Hypotheses	clmvscl.v	$$⊢V={\mathrm{Base}}_W$$
	clmvscl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	clmvscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	clmvscl.k	$$⊢K={\mathrm{Base}}_F$$
	clmvsdir.a	$$⊢\underset{\dot{}}{+}={+}_W$$
Assertion	clmvsdi	$$⊢\left(W\in \mathrm{CMod}\wedge \left(A\in K\wedge X\in V\wedge Y\in V\right)\right)\to A\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(A\underset{\dot{}}{·}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		clmvscl.v	$$⊢V={\mathrm{Base}}_W$$
2		clmvscl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		clmvscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		clmvscl.k	$$⊢K={\mathrm{Base}}_F$$
5		clmvsdir.a	$$⊢\underset{\dot{}}{+}={+}_W$$
6		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
7	1 5 2 3 4	lmodvsdi	$$⊢\left(W\in \mathrm{LMod}\wedge \left(A\in K\wedge X\in V\wedge Y\in V\right)\right)\to A\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(A\underset{\dot{}}{·}Y\right)$$
8	6 7	sylan	$$⊢\left(W\in \mathrm{CMod}\wedge \left(A\in K\wedge X\in V\wedge Y\in V\right)\right)\to A\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(A\underset{\dot{}}{·}Y\right)$$