clmvsass

Description: Associative law for scalar product. Analogue of lmodvsass . (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}$
Assertion	clmvsass	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to Q R \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (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	2	clmmul	$⊢ W \in CMod \to \times = \cdot_{F}$
6	5	adantr	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to \times = \cdot_{F}$
7	6	oveqd	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to Q R = Q \cdot_{F} R$
8	7	oveq1d	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to Q R \underset{˙}{\cdot} X = (Q \cdot_{F} R) \underset{˙}{\cdot} X$
9		clmlmod	$⊢ W \in CMod \to W \in LMod$
10		eqid	$⊢ \cdot_{F} = \cdot_{F}$
11	1 2 3 4 10	lmodvsass	$⊢ (W \in LMod \land (Q \in K \land R \in K \land X \in V)) \to (Q \cdot_{F} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
12	9 11	sylan	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to (Q \cdot_{F} R) \underset{˙}{\cdot} X = Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
13	8 12	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} (R \underset{˙}{\cdot} X)$

Metamath Proof Explorer