This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clmvsdi

Description: Distributive law for scalar product (left-distributivity). ( lmodvsdi analog.) (Contributed by NM, 3-Nov-2006) (Revised by AV, 28-Sep-2021)

		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	clmvsdi	$⊢ (W \in CMod \land (A \in K \land X \in V \land Y \in V)) \to A \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (A \underset{˙}{\cdot} X) \underset{˙}{+} (A \underset{˙}{\cdot} Y)$

Proof

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		clmlmod	$⊢ W \in CMod \to W \in LMod$
7	1 5 2 3 4	lmodvsdi	$⊢ (W \in LMod \land (A \in K \land X \in V \land Y \in V)) \to A \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (A \underset{˙}{\cdot} X) \underset{˙}{+} (A \underset{˙}{\cdot} Y)$
8	6 7	sylan	$⊢ (W \in CMod \land (A \in K \land X \in V \land Y \in V)) \to A \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (A \underset{˙}{\cdot} X) \underset{˙}{+} (A \underset{˙}{\cdot} Y)$