Metamath Proof Explorer

Theorem clmvscom

Description: Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008) (Revised by AV, 7-Oct-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}$
	Assertion	clmvscom	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) = R \underset{˙}{\cdot} (Q \underset{˙}{\cdot} X)$

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		ssel	$⊢ K \subseteq ℂ \to (Q \in K \to Q \in ℂ)$
6		ssel	$⊢ K \subseteq ℂ \to (R \in K \to R \in ℂ)$
7	5 6	anim12d	$⊢ K \subseteq ℂ \to ((Q \in K \land R \in K) \to (Q \in ℂ \land R \in ℂ))$
8	2 4	clmsscn	$⊢ W \in CMod \to K \subseteq ℂ$
9	7 8	syl11	$⊢ (Q \in K \land R \in K) \to (W \in CMod \to (Q \in ℂ \land R \in ℂ))$
10	9	3adant3	$⊢ (Q \in K \land R \in K \land X \in V) \to (W \in CMod \to (Q \in ℂ \land R \in ℂ))$
11	10	impcom	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to (Q \in ℂ \land R \in ℂ)$
12		mulcom	$⊢ (Q \in ℂ \land R \in ℂ) \to Q R = R Q$
13	11 12	syl	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to Q R = R Q$
14	13	oveq1d	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to Q R \underset{˙}{\cdot} X = R Q \underset{˙}{\cdot} X$
15	1 2 3 4	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)$
16		3ancoma	$⊢ (Q \in K \land R \in K \land X \in V) \leftrightarrow (R \in K \land Q \in K \land X \in V)$
17	1 2 3 4	clmvsass	$⊢ (W \in CMod \land (R \in K \land Q \in K \land X \in V)) \to R Q \underset{˙}{\cdot} X = R \underset{˙}{\cdot} (Q \underset{˙}{\cdot} X)$
18	16 17	sylan2b	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to R Q \underset{˙}{\cdot} X = R \underset{˙}{\cdot} (Q \underset{˙}{\cdot} X)$
19	14 15 18	3eqtr3d	$⊢ (W \in CMod \land (Q \in K \land R \in K \land X \in V)) \to Q \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) = R \underset{˙}{\cdot} (Q \underset{˙}{\cdot} X)$