Theorem clmsubdir

Description: Scalar multiplication distributive law for subtraction. ( lmodsubdir analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clmsubdir.v	$$⊢V={\mathrm{Base}}_W$$
	clmsubdir.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	clmsubdir.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	clmsubdir.k	$$⊢K={\mathrm{Base}}_F$$
	clmsubdir.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	clmsubdir.w	$$⊢\phi \to W\in \mathrm{CMod}$$
	clmsubdir.a	$$⊢\phi \to A\in K$$
	clmsubdir.b	$$⊢\phi \to B\in K$$
	clmsubdir.x	$$⊢\phi \to X\in V$$
Assertion	clmsubdir	$$⊢\phi \to \left(A-B\right)\underset{\dot{}}{·}X=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(B\underset{\dot{}}{·}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		clmsubdir.v	$$⊢V={\mathrm{Base}}_W$$
2		clmsubdir.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		clmsubdir.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		clmsubdir.k	$$⊢K={\mathrm{Base}}_F$$
5		clmsubdir.m	$$⊢\underset{\dot{}}{-}={-}_W$$
6		clmsubdir.w	$$⊢\phi \to W\in \mathrm{CMod}$$
7		clmsubdir.a	$$⊢\phi \to A\in K$$
8		clmsubdir.b	$$⊢\phi \to B\in K$$
9		clmsubdir.x	$$⊢\phi \to X\in V$$
10	3 4	clmsub	$$⊢\left(W\in \mathrm{CMod}\wedge A\in K\wedge B\in K\right)\to A-B=A{-}_{F}B$$
11	6 7 8 10	syl3anc	$$⊢\phi \to A-B=A{-}_{F}B$$
12	11	oveq1d	$$⊢\phi \to \left(A-B\right)\underset{\dot{}}{·}X=\left(A{-}_{F}B\right)\underset{\dot{}}{·}X$$
13		eqid	$$⊢{-}_F={-}_F$$
14		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
15	6 14	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
16	1 2 3 4 5 13 15 7 8 9	lmodsubdir	$$⊢\phi \to \left(A{-}_{F}B\right)\underset{\dot{}}{·}X=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(B\underset{\dot{}}{·}X\right)$$
17	12 16	eqtrd	$$⊢\phi \to \left(A-B\right)\underset{\dot{}}{·}X=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(B\underset{\dot{}}{·}X\right)$$