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

Metamath Proof Explorer

Theorem slmdvsdir

Description: Distributive law for scalar product. ( ax-hvdistr1 analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 22-Sep-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		slmdvsdir.v	$⊢ V = {Base}_{W}$
2		slmdvsdir.a	$⊢ \underset{˙}{+} = +_{W}$
3		slmdvsdir.f	$⊢ F = Scalar (W)$
4		slmdvsdir.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		slmdvsdir.k	$⊢ K = {Base}_{F}$
6		slmdvsdir.p	$⊢ \underset{˙}{⨣} = +_{F}$
7		eqid	$⊢ 0_{W} = 0_{W}$
8		eqid	$⊢ \cdot_{F} = \cdot_{F}$
9		eqid	$⊢ 1_{F} = 1_{F}$
10		eqid	$⊢ 0_{F} = 0_{F}$
11	1 2 4 7 3 5 6 8 9 10	slmdlema	$⊢ (W \in SLMod \land (Q \in K \land R \in K) \land (X \in V \land X \in V)) \to ((R \underset{˙}{\cdot} X \in V \land R \underset{˙}{\cdot} (X \underset{˙}{+} X) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X) \land (Q \underset{˙}{⨣} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)) \land ((Q \cdot_{F} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) \land 1_{F} \underset{˙}{\cdot} X = X \land 0_{F} \underset{˙}{\cdot} X = 0_{W}))$
12	11	simpld	$⊢ (W \in SLMod \land (Q \in K \land R \in K) \land (X \in V \land X \in V)) \to (R \underset{˙}{\cdot} X \in V \land R \underset{˙}{\cdot} (X \underset{˙}{+} X) = (R \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X) \land (Q \underset{˙}{⨣} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X))$
13	12	simp3d	$⊢ (W \in SLMod \land (Q \in K \land R \in K) \land (X \in V \land X \in V)) \to (Q \underset{˙}{⨣} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$
14	13	3expa	$⊢ ((W \in SLMod \land (Q \in K \land R \in K)) \land (X \in V \land X \in V)) \to (Q \underset{˙}{⨣} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$
15	14	anabsan2	$⊢ ((W \in SLMod \land (Q \in K \land R \in K)) \land X \in V) \to (Q \underset{˙}{⨣} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$
16	15	exp42	$⊢ W \in SLMod \to (Q \in K \to (R \in K \to (X \in V \to (Q \underset{˙}{⨣} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X))))$
17	16	3imp2	$⊢ (W \in SLMod \land (Q \in K \land R \in K \land X \in V)) \to (Q \underset{˙}{⨣} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) \underset{˙}{+} (R \underset{˙}{\cdot} X)$