ax-hvmulass

Description: Scalar multiplication associative law. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax-hvmulass	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℋ) \to A B \cdot_{ℎ} C = A \cdot_{ℎ} (B \cdot_{ℎ} C)$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cc	$class ℂ$
2	0 1	wcel	$wff A \in ℂ$
3		cB	$class B$
4	3 1	wcel	$wff B \in ℂ$
5		cC	$class C$
6		chba	$class ℋ$
7	5 6	wcel	$wff C \in ℋ$
8	2 4 7	w3a	$wff (A \in ℂ \land B \in ℂ \land C \in ℋ)$
9		cmul	$class \times$
10	0 3 9	co	$class A B$
11		csm	$class \cdot_{ℎ}$
12	10 5 11	co	$class (A B \cdot_{ℎ} C)$
13	3 5 11	co	$class (B \cdot_{ℎ} C)$
14	0 13 11	co	$class (A \cdot_{ℎ} (B \cdot_{ℎ} C))$
15	12 14	wceq	$wff A B \cdot_{ℎ} C = A \cdot_{ℎ} (B \cdot_{ℎ} C)$
16	8 15	wi	$wff ((A \in ℂ \land B \in ℂ \land C \in ℋ) \to A B \cdot_{ℎ} C = A \cdot_{ℎ} (B \cdot_{ℎ} C))$

Metamath Proof Explorer