clmvsdir

Description: Distributive law for scalar product (right-distributivity). ( lmodvsdir analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clmvscl.v	$⊢ V = {Base}_{W}$
	clmvscl.f	$⊢ F = Scalar (W)$
	clmvscl.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	clmvscl.k	$⊢ K = {Base}_{F}$
	clmvsdir.a	$⊢ \underset{˙}{+} = +_{W}$
Assertion	clmvsdir	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to (Q + R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$

Step	Hyp	Ref	Expression
1		clmvscl.v	$⊢ V = {Base}_{W}$
2		clmvscl.f	$⊢ F = Scalar (W)$
3		clmvscl.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		clmvscl.k	$⊢ K = {Base}_{F}$
5		clmvsdir.a	$⊢ \underset{˙}{+} = +_{W}$
6	2	clmadd	$⊢ W \in CMod \to + = +_{F}$
7	6	oveqd	$⊢ W \in CMod \to Q + R = Q +_{F} R$
8	7	oveq1d	$⊢ W \in CMod \to (Q + R) \underset{˙}{\cdot} X = (Q +_{F} R) \underset{˙}{\cdot} X$
9	8	adantr	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to (Q + R) \underset{˙}{\cdot} X = (Q +_{F} R) \underset{˙}{\cdot} X$
10		clmlmod	$⊢ W \in CMod \to W \in LMod$
11		eqid	$⊢ +_{F} = +_{F}$
12	1 5 2 3 4 11	lmodvsdir	$⊢ (W \in LMod \land (Q \in K \land R \in K \land X \in V)) \to (Q +_{F} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$
13	10 12	sylan	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to (Q +_{F} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$
14	9 13	eqtrd	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to (Q + R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$

Metamath Proof Explorer