Theorem lmodvsdir

Description: Distributive law for scalar product (right-distributivity). ( ax-hvdistr1 analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 22-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lmodvsdir.v	$$⊢V={\mathrm{Base}}_W$$
2		lmodvsdir.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lmodvsdir.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lmodvsdir.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		lmodvsdir.k	$$⊢K={\mathrm{Base}}_F$$
6		lmodvsdir.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
7		eqid	$$⊢{\cdot }_F={\cdot }_F$$
8		eqid	$$⊢1_F=1_F$$
9	1 2 4 3 5 6 7 8	lmodlema	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\wedge \left(X\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{}}{+}X\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}X=\left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\right)\wedge \left(\left(Q{\cdot }_{F}R\right)\underset{\dot{}}{·}X=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}X\right)\wedge 1_F\underset{\dot{}}{·}X=X\right)\right)$$
10	9	simpld	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\wedge \left(X\in V\wedge X\in V\right)\right)\to \left(R\underset{\dot{}}{·}X\in V\wedge R\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}X=\left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\right)$$
11	10	simp3d	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\wedge \left(X\in V\wedge X\in V\right)\right)\to \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}X=\left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)$$
12	11	3expa	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\right)\wedge \left(X\in V\wedge X\in V\right)\right)\to \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}X=\left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)$$
13	12	anabsan2	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\right)\wedge X\in V\right)\to \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}X=\left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)$$
14	13	exp42	$$⊢W\in \mathrm{LMod}\to \left(Q\in K\to \left(R\in K\to \left(X\in V\to \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}X=\left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\right)\right)\right)$$
15	14	3imp2	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\wedge X\in V\right)\right)\to \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}X=\left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)$$