Theorem hvmulassi

Description: Scalar multiplication associative 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 \mathscr{H}$$
Assertion	hvmulassi	$$⊢AB{\cdot }_{ℎ}C=A{\cdot }_{ℎ}\left(B{\cdot }_{ℎ}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvmulcom.1	$$⊢A\in ℂ$$
2		hvmulcom.2	$$⊢B\in ℂ$$
3		hvmulcom.3	$$⊢C\in \mathscr{H}$$
4		ax-hvmulass	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in \mathscr{H}\right)\to AB{\cdot }_{ℎ}C=A{\cdot }_{ℎ}\left(B{\cdot }_{ℎ}C\right)$$
5	1 2 3 4	mp3an	$$⊢AB{\cdot }_{ℎ}C=A{\cdot }_{ℎ}\left(B{\cdot }_{ℎ}C\right)$$