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

Metamath Proof Explorer

Theorem lmodvsdi

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

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

Proof

Step	Hyp	Ref	Expression
1		lmodvsdi.v	$⊢ V = {Base}_{W}$
2		lmodvsdi.a	$⊢ \underset{˙}{+} = +_{W}$
3		lmodvsdi.f	$⊢ F = Scalar (W)$
4		lmodvsdi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		lmodvsdi.k	$⊢ K = {Base}_{F}$
6		eqid	$⊢ +_{F} = +_{F}$
7		eqid	$⊢ \cdot_{F} = \cdot_{F}$
8		eqid	$⊢ 1_{F} = 1_{F}$
9	1 2 4 3 5 6 7 8	lmodlema	$⊢ (W \in LMod \land (R \in K \land R \in K) \land (Y \in V \land X \in V)) \to ((R \underset{˙}{\cdot} X \in V \land R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y) \land (R +_{F} R) \underset{˙}{\cdot} X = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)) \land ((R \cdot_{F} R) \underset{˙}{\cdot} X = R \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) \land 1_{F} \underset{˙}{\cdot} X = X))$
10	9	simpld	$⊢ (W \in LMod \land (R \in K \land R \in K) \land (Y \in V \land X \in V)) \to (R \underset{˙}{\cdot} X \in V \land R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y) \land (R +_{F} R) \underset{˙}{\cdot} X = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X))$
11	10	simp2d	$⊢ (W \in LMod \land (R \in K \land R \in K) \land (Y \in V \land X \in V)) \to R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y)$
12	11	3expia	$⊢ (W \in LMod \land (R \in K \land R \in K)) \to ((Y \in V \land X \in V) \to R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y))$
13	12	anabsan2	$⊢ (W \in LMod \land R \in K) \to ((Y \in V \land X \in V) \to R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y))$
14	13	exp4b	$⊢ W \in LMod \to (R \in K \to (Y \in V \to (X \in V \to R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y))))$
15	14	com34	$⊢ W \in LMod \to (R \in K \to (X \in V \to (Y \in V \to R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y))))$
16	15	3imp2	$⊢ (W \in LMod \land (R \in K \land X \in V \land Y \in V)) \to R \underset{˙}{\cdot} (X \underset{˙}{+} Y) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} Y)$