Theorem slmdvsdi

Description: Distributive law for scalar product. ( ax-hvdistr1 analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 22-Sep-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		slmdvsdi.v	$$⊢V={\mathrm{Base}}_W$$
2		slmdvsdi.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		slmdvsdi.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		slmdvsdi.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		slmdvsdi.k	$$⊢K={\mathrm{Base}}_F$$
6		eqid	$$⊢0_W=0_W$$
7		eqid	$$⊢{+}_F={+}_F$$
8		eqid	$$⊢{\cdot }_F={\cdot }_F$$
9		eqid	$$⊢1_F=1_F$$
10		eqid	$$⊢0_F=0_F$$
11	1 2 4 6 3 5 7 8 9 10	slmdlema	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(R\in K\wedge R\in K\right)\wedge \left(Y\in V\wedge X\in V\right)\right)\to \left(\left(R\underset{\dot{}}{·}X\in V\wedge R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\wedge \left(R{+}_{F}R\right)\underset{\dot{}}{·}X=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\right)\wedge \left(\left(R{\cdot }_{F}R\right)\underset{\dot{}}{·}X=R\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}X\right)\wedge 1_F\underset{\dot{}}{·}X=X\wedge 0_F\underset{\dot{}}{·}X=0_W\right)\right)$$
12	11	simpld	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(R\in K\wedge R\in K\right)\wedge \left(Y\in V\wedge X\in V\right)\right)\to \left(R\underset{\dot{}}{·}X\in V\wedge R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\wedge \left(R{+}_{F}R\right)\underset{\dot{}}{·}X=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\right)$$
13	12	simp2d	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(R\in K\wedge R\in K\right)\wedge \left(Y\in V\wedge X\in V\right)\right)\to R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)$$
14	13	3expia	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(R\in K\wedge R\in K\right)\right)\to \left(\left(Y\in V\wedge X\in V\right)\to R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)$$
15	14	anabsan2	$$⊢\left(W\in \mathrm{SLMod}\wedge R\in K\right)\to \left(\left(Y\in V\wedge X\in V\right)\to R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)$$
16	15	exp4b	$$⊢W\in \mathrm{SLMod}\to \left(R\in K\to \left(Y\in V\to \left(X\in V\to R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\right)\right)$$
17	16	com34	$$⊢W\in \mathrm{SLMod}\to \left(R\in K\to \left(X\in V\to \left(Y\in V\to R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\right)\right)$$
18	17	3imp2	$$⊢\left(W\in \mathrm{SLMod}\wedge \left(R\in K\wedge X\in V\wedge Y\in V\right)\right)\to R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)$$