ax-hvdistr2

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

		Ref	Expression
	Assertion	ax-hvdistr2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℋ) \to (A + B) \cdot_{ℎ} C = (A \cdot_{ℎ} C) +_{ℎ} (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		caddc	$class +$
10	0 3 9	co	$class (A + B)$
11		csm	$class \cdot_{ℎ}$
12	10 5 11	co	$class ((A + B) \cdot_{ℎ} C)$
13	0 5 11	co	$class (A \cdot_{ℎ} C)$
14		cva	$class +_{ℎ}$
15	3 5 11	co	$class (B \cdot_{ℎ} C)$
16	13 15 14	co	$class ((A \cdot_{ℎ} C) +_{ℎ} (B \cdot_{ℎ} C))$
17	12 16	wceq	$wff (A + B) \cdot_{ℎ} C = (A \cdot_{ℎ} C) +_{ℎ} (B \cdot_{ℎ} C)$
18	8 17	wi	$wff ((A \in ℂ \land B \in ℂ \land C \in ℋ) \to (A + B) \cdot_{ℎ} C = (A \cdot_{ℎ} C) +_{ℎ} (B \cdot_{ℎ} C))$

Metamath Proof Explorer