clmsubdir

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

	Ref	Expression
Hypotheses	clmsubdir.v	$⊢ V = {Base}_{W}$
	clmsubdir.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	clmsubdir.f	$⊢ F = Scalar (W)$
	clmsubdir.k	$⊢ K = {Base}_{F}$
	clmsubdir.m	$⊢ \underset{˙}{-} = -_{W}$
	clmsubdir.w	$⊢ φ \to W \in CMod$
	clmsubdir.a	$⊢ φ \to A \in K$
	clmsubdir.b	$⊢ φ \to B \in K$
	clmsubdir.x	$⊢ φ \to X \in V$
Assertion	clmsubdir	$⊢ φ \to (A - B) \underset{˙}{\cdot} X = (A \underset{˙}{\cdot} X) \underset{˙}{-} (B \underset{˙}{\cdot} X)$

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

Metamath Proof Explorer