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

Metamath Proof Explorer

Theorem lmodvsass

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

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

Proof

Step	Hyp	Ref	Expression
1		lmodvsass.v	$⊢ V = {Base}_{W}$
2		lmodvsass.f	$⊢ F = Scalar (W)$
3		lmodvsass.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodvsass.k	$⊢ K = {Base}_{F}$
5		lmodvsass.t	$⊢ \underset{˙}{\times} = \cdot_{F}$
6		eqid	$⊢ +_{W} = +_{W}$
7		eqid	$⊢ +_{F} = +_{F}$
8		eqid	$⊢ 1_{F} = 1_{F}$
9	1 6 3 2 4 7 5 8	lmodlema	$⊢ (W \in LMod \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 +_{W} X) = (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X) \land (Q +_{F} R) \underset{˙}{\cdot} X = (Q \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X)) \land ((Q \underset{˙}{\times} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) \land 1_{F} \underset{˙}{\cdot} X = X))$
10	9	simprld	$⊢ (W \in LMod \land (Q \in K \land R \in K) \land (X \in V \land X \in V)) \to (Q \underset{˙}{\times} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
11	10	3expa	$⊢ ((W \in LMod \land (Q \in K \land R \in K)) \land (X \in V \land X \in V)) \to (Q \underset{˙}{\times} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
12	11	anabsan2	$⊢ ((W \in LMod \land (Q \in K \land R \in K)) \land X \in V) \to (Q \underset{˙}{\times} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
13	12	exp42	$⊢ W \in LMod \to (Q \in K \to (R \in K \to (X \in V \to (Q \underset{˙}{\times} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X))))$
14	13	3imp2	$⊢ (W \in LMod \land (Q \in K \land R \in K \land X \in V)) \to (Q \underset{˙}{\times} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$