Metamath Proof Explorer

Theorem hvmulcomi

Description: Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvmulcom.1	$⊢ A \in ℂ$
	hvmulcom.2	$⊢ B \in ℂ$
	hvmulcom.3	$⊢ C \in ℋ$
Assertion	hvmulcomi	$⊢ A \cdot_{ℎ} (B \cdot_{ℎ} C) = B \cdot_{ℎ} (A \cdot_{ℎ} C)$

Step	Hyp	Ref	Expression
1		hvmulcom.1	$⊢ A \in ℂ$
2		hvmulcom.2	$⊢ B \in ℂ$
3		hvmulcom.3	$⊢ C \in ℋ$
4		hvmulcom	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℋ) \to A \cdot_{ℎ} (B \cdot_{ℎ} C) = B \cdot_{ℎ} (A \cdot_{ℎ} C)$
5	1 2 3 4	mp3an	$⊢ A \cdot_{ℎ} (B \cdot_{ℎ} C) = B \cdot_{ℎ} (A \cdot_{ℎ} C)$